Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added map/burrow_facts;
authorwenzelm
Wed, 29 Nov 2006 23:28:10 +0100
changeset 21597 0e7a441ac637
parent 21596 486cae91868f
child 21598 2b702007e7c8
added map/burrow_facts; exported name_multi, name_thm;
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle