diff -r 486cae91868f -r 0e7a441ac637 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Nov 29 23:28:08 2006 +0100
+++ b/src/Pure/pure_thy.ML	Wed Nov 29 23:28:10 2006 +0100
@@ -418,10 +418,7 @@
   | smart_store name_thm (name, [thm]) =
       fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
   | smart_store name_thm (name, thms) =
-      let
-        fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th)
-          handle TERM (msg, _) => raise THM (msg, 0, [th]);
-        val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
+      let val thy = Theory.merge_list (map Thm.theory_of_thm thms)
       in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
 
 in