# HG changeset patch
# User clasohm
# Date 786800087 -3600
# Node ID e0b172d01c3764f3bfd9cec0393735113323efa1
# Parent  c2b210bda7108a54e7125c2542f8cb99ea6f72b8
moved first call of store_theory from thy_read.ML to created .thy.ML file

diff -r c2b210bda710 -r e0b172d01c37 src/Pure/Thy/thy_parse.ML
--- 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;
-
diff -r c2b210bda710 -r e0b172d01c37 src/Pure/Thy/thy_read.ML
--- 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 ()