src/Pure/Thy/thy_read.ML

 
   val use_thy        : string -> unit
   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
   val theory_of_thm: thm -> theory
   val store_thm: string * thm -> thm

      reload_changed (load_order ["Pure"] [])
   end;
 
 (*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
                 in if is_some tinfo then
                      let val ThyInfo {children, ...} = the tinfo