# HG changeset patch
# User wenzelm
# Date 1164892651 -3600
# Node ID dc75da2cb7d1e4cfaedf8d073ddaed5b38ad86dc
# Parent  4e7307e229b32ebfd771fc8bfb4589b86e91f7f3
Theory.merge_list;

diff -r 4e7307e229b3 -r dc75da2cb7d1 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Nov 30 14:17:29 2006 +0100
+++ b/src/Pure/pure_thy.ML	Thu Nov 30 14:17:31 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