# HG changeset patch
# User wenzelm
# Date 876921322 -7200
# Node ID e6f918979f2d1a3ac4374a9b1d515a3b48eb9e47
# Parent  f62a4edb18883f07b929ca6fe35f8bd7791f4dfc
tuned;

diff -r f62a4edb1888 -r e6f918979f2d src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed Oct 15 15:14:56 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed Oct 15 15:15:22 1997 +0200
@@ -21,7 +21,7 @@
   val exit_use_dir   : string -> unit
   val update         : unit -> unit
   val unlink_thy     : string -> unit
-  val mk_base        : basetype list -> string -> bool -> theory
+  val mk_base        : basetype list -> string -> theory
 end;
 
 
@@ -404,7 +404,7 @@
 
 (*Merge theories to build a base for a new theory.
   Base members are only loaded if they are missing.*)
-fun mk_base bases child mk_draft =
+fun mk_base bases child =
   let (*Show the cycle that would be created by add_child*)
       fun show_cycle base =
         let fun find_it result curr =
@@ -456,8 +456,8 @@
               (find_cycle base;
                add_child base;
                if thy_loaded then ()
-               else (writeln ("Autoloading theory " ^ (quote base)
-                              ^ " (used by " ^ (quote child) ^ ")");
+               else (writeln ("Autoloading theory " ^ quote base
+                              ^ " (required by " ^ quote child ^ ")");
                      use_thy1 true base)
               )
           end;
@@ -474,8 +474,9 @@
       val dummy = unlink_thy child;
       val mergelist = load_base bases;
 
-      val base_thy = (writeln ("Loading theory " ^ (quote child));
-                      Theory.merge_thy_list mk_draft (map theory_of mergelist));
+      val base_thy =
+       (writeln ("Loading theory " ^ quote child);
+        Theory.merge_list (map theory_of mergelist));
 
       val datas =
         let fun get_data t =
diff -r f62a4edb1888 -r e6f918979f2d src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Wed Oct 15 15:14:56 1997 +0200
+++ b/src/Pure/name_space.ML	Wed Oct 15 15:15:22 1997 +0200
@@ -25,7 +25,7 @@
   val prune: T -> string -> string
 end;
 
-structure NameSpace(*: NAME_SPACE FIXME *) =
+structure NameSpace: NAME_SPACE =
 struct
 
 
@@ -61,7 +61,7 @@
 
 fun make entries =
   let
-    fun accesses [] = []		(* FIXME !? *)
+    fun accesses [] = []
       | accesses entry =
           let
             val p = pack entry;