--- a/src/Pure/pure_thy.ML Wed Nov 29 23:28:13 2006 +0100
+++ b/src/Pure/pure_thy.ML Wed Nov 29 23:33:09 2006 +0100
@@ -418,7 +418,10 @@
| 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 val thy = Theory.merge_list (map Thm.theory_of_thm 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));
in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
in