src/Pure/Thy/thy_parse.ML

 
 
 (* header *)
 
 fun mk_header (thy_name, bases) =
-  (thy_name, "base_on " ^ mk_list bases ^ " " ^ quote thy_name);
+  (thy_name, "mk_base " ^ mk_list bases ^ " " ^ quote thy_name);
 
 val base =
   ident >> (cat "Thy" o quote) ||
   string >> cat "File";
 

     error ("Filename \"" ^ tname ^ ".thy\" and theory name "
       ^ quote thy_name ^ " are different")
   else
     (case opt_txts of
       Some (extxt, postxt, mltxt) =>
-        "structure " ^ thy_name ^ " =\n\
+        "val base = " ^ old_thys ^ " true;\n\n\
+        \structure " ^ thy_name ^ " =\n\
         \struct\n\
         \\n\
         \local\n"
         ^ trfun_defs ^ "\n\
         \in\n\
         \\n"
         ^ mltxt ^ "\n\
         \\n\
-        \val thy = (" ^ old_thys ^ " true)\n\n\
+        \val thy = base\n\n\
         \|> add_trfuns\n"
         ^ trfun_args ^ "\n\
         \\n"
         ^ extxt ^ "\n\
         \\n\

         ^ postxt ^ "\n\
         \\n\
         \end;\n\
         \end;\n"
     | None =>
-        "structure " ^ thy_name ^ " =\n\
+        "val base = " ^ old_thys ^ " false;\n\n\
+        \structure " ^ thy_name ^ " =\n\
         \struct\n\
         \\n\
-        \val thy = (" ^ old_thys ^ " false);\n\
+        \val thy = base\n\
         \\n\
         \end;\n");
 
 fun theory_defn sectab tname =
   header -- optional (extension sectab >> Some) None -- eof