# HG changeset patch
# User wenzelm
# Date 877706329 -7200
# Node ID 6ec8d42082f1c3ec0f2e0531000afe24d33b0441
# Parent  42062f636bdf5640818916f5d867125ffe075724
merge: default to ProtoPure.thy;

diff -r 42062f636bdf -r 6ec8d42082f1 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 =