# 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