# HG changeset patch
# User wenzelm
# Date 771761216 -7200
# Node ID f9d7e4fe141a38ccf591688853b12b9a7cf31dd4
# Parent  a42892e72854c962e8f7d73c0fbd799a6096d870
base_on: added 'mk_draft' arg;

diff -r a42892e72854 -r f9d7e4fe141a 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