base_on: added 'mk_draft' arg;
authorwenzelm
Thu, 16 Jun 1994 12:06:56 +0200
changeset 424 f9d7e4fe141a
parent 423 a42892e72854
child 425 c42f384c89de
base_on: added 'mk_draft' arg;
src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Jun 16 12:05:53 1994 +0200
+++ b/src/Pure/Thy/thy_read.ML	Thu Jun 16 12:06:56 1994 +0200
@@ -28,7 +28,7 @@
   val update         : unit -> unit
   val time_use_thy   : string -> unit
   val unlink_thy     : string -> unit
-  val base_on        : basetype list -> string -> Thm.theory
+  val base_on        : basetype list -> string -> bool -> Thm.theory
   val store_theory   : string -> Thm.theory -> unit
 end;
 
@@ -343,7 +343,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 =
+fun base_on bases child mk_draft =
       let (*List all descendants of a theory list *)
           fun list_descendants (t :: ts) =
                 let val tinfo = get_thyinfo t