src/Pure/Thy/thy_parse.ML
changeset 759 e0b172d01c37
parent 710 53fef17a729a
child 777 c007eba368b7
     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 -