merge: default to ProtoPure.thy;
authorwenzelm
Fri, 24 Oct 1997 17:18:49 +0200
changeset 3998 6ec8d42082f1
parent 3997 42062f636bdf
child 3999 86c5bda38e9f
merge: default to ProtoPure.thy;
src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Oct 24 17:18:25 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Fri Oct 24 17:18:49 1997 +0200
@@ -476,7 +476,8 @@
 
       val base_thy =
        (writeln ("Loading theory " ^ quote child);
-        Theory.prep_ext_merge (map theory_of mergelist));
+         if null mergelist then ProtoPure.thy
+         else Theory.prep_ext_merge (map theory_of mergelist));
 
       val datas =
         let fun get_data t =