--- 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;
-
--- a/src/Pure/Thy/thy_read.ML Tue Dec 06 12:50:13 1994 +0100
+++ b/src/Pure/Thy/thy_read.ML Wed Dec 07 12:34:47 1994 +0100
@@ -255,11 +255,7 @@
if thy_uptodate orelse thy_file = "" then ()
else (writeln ("Reading \"" ^ name ^ ".thy\"");
read_thy tname thy_file;
- use (out_name tname);
- use_string
- ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]
- (*Store theory object in case it is needed for store_thm
- while reading the ML file*)
+ use (out_name tname)
);
if ml_file = "" then ()