diff -r 075db6ac7f2f -r 208ab8773a73 src/Pure/Thy/syntax.ML
--- a/src/Pure/Thy/syntax.ML	Fri Oct 22 13:39:23 1993 +0100
+++ b/src/Pure/Thy/syntax.ML	Fri Oct 22 13:42:51 1993 +0100
@@ -112,7 +112,8 @@
     axs ^ "\n\n" ^ vals
   end;
 
-fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend\n";
+fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"
+                        ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n";
 
 
 fun mk_sext mfix trans =
@@ -148,22 +149,20 @@
       let
         val noext = ("[]", "[]", "[]", "[]", "[]", "[]");
         val basethy =
-          if tinfix = "[]" then base
-          else mk_ext_thy (base, name ^ "(type infix)", noext, mk_simple_sext tinfix);
+          if tinfix = "[]" then base ^ (quote name)
+          else mk_ext_thy (base ^ (quote name), name ^ "(type infix)", noext, mk_simple_sext tinfix);
         val sext =
           if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None"
           else mk_sext mfix trans;
-        val thy = "\nval thy = " ^ mk_ext_thy (basethy, name, ext, sext);
+        val thy = "val thy = " ^ mk_ext_thy (basethy, name, ext, sext);
       in
         mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend")
       end
-  | mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base);
-
+  | mk_structure ((name, base), None) =
+      mk_struct (name, "\nval thy = " ^ base ^ (quote name));
 
-fun merge (t :: ts) =
-      foldl (fn (base, thy) => "(merge_theories (" ^ base ^ ", " ^ thy ^ ".thy))")
-        (t ^ ".thy", ts)
-  | merge [] = raise Match;
+fun merge thys =
+  "base_on " ^ (bracket (quote (space_implode "\",\"" thys))) ^ " ";