diff --git a/src/1/theory_tests/gh1370Script.sml b/src/1/theory_tests/gh1370Script.sml new file mode 100644 index 0000000000..7a1aa2a208 --- /dev/null +++ b/src/1/theory_tests/gh1370Script.sml @@ -0,0 +1,15 @@ +open HolKernel boolLib + +val _ = new_theory"gh1370"; + +val _ = new_definition ("def", “c = T”); + +val _ = + adjoin_to_theory + {sig_ps = SOME (fn _ => PP.add_string "val ctm : Term.term"), + struct_ps = NONE}; + +val _ = adjoin_after_completion + (fn _ => PP.add_string ("val ctm = Parse.Term ‘c’;\n\n")) + +val _ = export_theory(); diff --git a/src/1/theory_tests/gh1370childScript.sml b/src/1/theory_tests/gh1370childScript.sml new file mode 100644 index 0000000000..f7493ac403 --- /dev/null +++ b/src/1/theory_tests/gh1370childScript.sml @@ -0,0 +1,11 @@ +open HolKernel Parse boolLib + +open gh1370Theory + +val _ = new_theory "gh1370child"; + +val _ = type_of gh1370Theory.ctm = bool andalso + (print "ctm has correct type\n";true) orelse + OS.Process.exit OS.Process.failure + +val _ = export_theory();