# HG changeset patch
# User clasohm
# Date 771849804 -7200
# Node ID 767367131b4745560a108e06c8b0ae66a16ed47c
# Parent  c42f384c89de8bea98b950b77e0743cd7958062d
replaced "foldl merge_theories" by "merge_thy_list" in base_on

diff -r c42f384c89de -r 767367131b47 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Jun 16 12:07:40 1994 +0200
+++ b/src/Pure/Thy/thy_read.ML	Fri Jun 17 12:43:24 1994 +0200
@@ -390,14 +390,14 @@
                       end
                   | add [] =
                       [ThyInfo {name = base, path = "", children = [child], 
-                                thy_info = None, ml_info = None, theory = None}]
+                               thy_info = None, ml_info = None, theory = None}]
             in loaded_thys := add (!loaded_thys) end;       
 
           (*Load a base theory if not already done
             and no cycle would be created *)
           fun load base =
               let val thy_present = already_loaded base
-                                            (*test this before child is added *)
+                                           (*test this before child is added *)
               in
                 if child = base then
                     error ("Cyclic dependency of theories: " ^ child
@@ -428,10 +428,8 @@
 
           val mergelist = (unlink_thy child;
                            load_base bases);
-          val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
-                                               (*we have to return something *)
      in writeln ("Loading theory " ^ (quote child));
-        foldl Thm.merge_theories (get_theory t, map get_theory ts) end;
+        merge_thy_list mk_draft (map get_theory mergelist) end;
 
 (*Change theory object for an existent item of loaded_thys 
   or create a new item *)