src/Pure/Thy/thy_parse.ML

         \\n\
         \\n"
         ^ 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\
         \struct\n\
         \\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
   >> (mk_structure tname o #1);
 

   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   ("instance", instance_decl)];
 
 
 end;
-