--- a/src/Pure/Thy/thy_parse.ML Tue Dec 06 12:50:13 1994 +0100
+++ b/src/Pure/Thy/thy_parse.ML Wed Dec 07 12:34:47 1994 +0100
@@ -415,7 +415,8 @@
^ postxt ^ "\n\
\\n\
\end;\n\
- \end;\n"
+ \end;\n\n\
+ \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n"
| None =>
"val thy = " ^ old_thys ^ " false;\n\n\
\structure " ^ thy_name ^ " =\n\
@@ -423,7 +424,8 @@
\\n\
\val thy = thy\n\
\\n\
- \end;\n");
+ \end;\n\n\
+ \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n");
fun theory_defn sectab tname =
header -- optional (extension sectab >> Some) None -- eof
@@ -468,4 +470,3 @@
end;
-