moved first call of store_theory from thy_read.ML to created .thy.ML file
authorclasohm
Wed Dec 07 12:34:47 1994 +0100 (1994-12-07)
changeset 759e0b172d01c37
parent 758 c2b210bda710
child 760 f0200e91b272
moved first call of store_theory from thy_read.ML to created .thy.ML file
src/Pure/Thy/thy_parse.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Dec 06 12:50:13 1994 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Dec 07 12:34:47 1994 +0100
     1.3 @@ -415,7 +415,8 @@
     1.4          ^ postxt ^ "\n\
     1.5          \\n\
     1.6          \end;\n\
     1.7 -        \end;\n"
     1.8 +        \end;\n\n\
     1.9 +        \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n"
    1.10      | None =>
    1.11          "val thy = " ^ old_thys ^ " false;\n\n\
    1.12          \structure " ^ thy_name ^ " =\n\
    1.13 @@ -423,7 +424,8 @@
    1.14          \\n\
    1.15          \val thy = thy\n\
    1.16          \\n\
    1.17 -        \end;\n");
    1.18 +        \end;\n\n\
    1.19 +        \store_theory (" ^ thy_name ^ ".thy, " ^ quote thy_name ^ ");\n");
    1.20  
    1.21  fun theory_defn sectab tname =
    1.22    header -- optional (extension sectab >> Some) None -- eof
    1.23 @@ -468,4 +470,3 @@
    1.24  
    1.25  
    1.26  end;
    1.27 -
     2.1 --- a/src/Pure/Thy/thy_read.ML	Tue Dec 06 12:50:13 1994 +0100
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Wed Dec 07 12:34:47 1994 +0100
     2.3 @@ -255,11 +255,7 @@
     2.4           if thy_uptodate orelse thy_file = "" then ()
     2.5           else (writeln ("Reading \"" ^ name ^ ".thy\"");
     2.6                 read_thy tname thy_file;
     2.7 -               use (out_name tname);
     2.8 -               use_string
     2.9 -                 ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]
    2.10 -                       (*Store theory object in case it is needed for store_thm
    2.11 -                         while reading the ML file*)
    2.12 +               use (out_name tname)
    2.13                );
    2.14  
    2.15           if ml_file = "" then ()