# HG changeset patch
# User clasohm
# Date 778855450 -7200
# Node ID 201e115d803199dab31cdb242b7273a113c92a49
# Parent  409c9ee7a9f30fbfb9ad5cf127037c64468cb9ae
renamed base_on into mk_base and moved it to the beginning of the generated
.thy.ML file to make sure that all base theories are present when ML executes
the rest of this file

diff -r 409c9ee7a9f3 -r 201e115d8031 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Sep 06 13:46:53 1994 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Tue Sep 06 14:44:10 1994 +0200
@@ -350,7 +350,7 @@
 (* 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) ||
@@ -389,7 +389,8 @@
   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"
@@ -398,7 +399,7 @@
         \\n"
         ^ mltxt ^ "\n\
         \\n\
-        \val thy = (" ^ old_thys ^ " true)\n\n\
+        \val thy = base\n\n\
         \|> add_trfuns\n"
         ^ trfun_args ^ "\n\
         \\n"
@@ -412,10 +413,11 @@
         \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");
 
diff -r 409c9ee7a9f3 -r 201e115d8031 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Tue Sep 06 13:46:53 1994 +0200
+++ b/src/Pure/Thy/thy_read.ML	Tue Sep 06 14:44:10 1994 +0200
@@ -33,7 +33,7 @@
   val update         : unit -> unit
   val time_use_thy   : string -> unit
   val unlink_thy     : string -> unit
-  val base_on        : basetype list -> string -> bool -> theory
+  val mk_base        : basetype list -> string -> bool -> theory
   val store_theory   : theory * string -> unit
 
   val theory_of_sign: Sign.sg -> theory
@@ -333,7 +333,7 @@
 
 (*Merge theories to build a base for a new theory.
   Base members are only loaded if they are missing. *)
-fun base_on bases child mk_draft =
+fun mk_base bases child mk_draft =
       let (*List all descendants of a theory list *)
           fun list_descendants (t :: ts) =
                 let val tinfo = get_thyinfo t