src/Pure/Thy/syntax.ML

 Definition of theory syntax together with translation to ML code.
 *)
 
 signature THYSYN =
  sig
-  datatype BaseType = Thy  of string
+  datatype basetype = Thy  of string
                     | File of string
 
    val read: string list -> string
  end;
 

     val vals = foldr add_val (ps, "")
   in
     axs ^ "\n\n" ^ vals
   end;
 
-fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"
-                        ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n";
+fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n";
 
 
 fun mk_sext mfix trans =
   "Some (NewSext {\n\
 \   mixfix =\n    " ^ mfix ^ ",\n\

         mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend")
       end
   | mk_structure ((name, base), None) =
       mk_struct (name, "\nval thy = " ^ base ^ (quote name));
 
-datatype BaseType = Thy  of string
+datatype basetype = Thy  of string
                   | File of string;
 
 fun merge thys =
   let fun make_list (Thy t :: ts) =
             ("Thy \"" ^ t ^ "\"") :: make_list ts