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.
Theory.merge_list;
authorwenzelm
Thu, 30 Nov 2006 14:17:31 +0100
changeset 21606 dc75da2cb7d1
parent 21605 4e7307e229b3
child 21607 3698319f6503
Theory.merge_list;
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle