--- a/src/Pure/Thy/thy_parse.ML Wed Nov 27 16:36:36 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML Wed Nov 27 16:40:23 1996 +0100
@@ -486,7 +486,10 @@
^ postxt ^ "\n\
\\n\
\end;\n\
- \end;\n"
+ \end;\n\
+ \\n\
+ \open " ^ thy_name ^ ";\n\
+ \\n"
| None =>
"val thy = " ^ old_thys ^ " false;\n\
\\n\
@@ -497,7 +500,11 @@
\\n\
\val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
\\n\
- \end;\n");
+ \end;\n\
+ \\n\
+ \open " ^ thy_name ^ ";\n\
+ \\n");
+
fun theory_defn sectab tname =
header -- optional (extension sectab >> Some) None -- eof