Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/shuffler.ML
changeset 33038 8f9594c31de4
parent 33037 b22e44496dc2
child 33040 cffdb7b28498
child 33042 ddf1f03a9ad9 
--- a/src/HOL/Import/shuffler.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/Import/shuffler.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -78,7 +78,7 @@
   val empty = []
   val copy = I
   val extend = I
-  fun merge _ = Library.gen_union Thm.eq_thm
+  fun merge _ = Library.union Thm.eq_thm
 )
 
 fun print_shuffles thy =
@@ -563,7 +563,7 @@
         let
             val th_consts = add_consts(prop_of th,[])
         in
-            gen_eq_set (op =) (t_consts, th_consts)
+            eq_set (op =) (t_consts, th_consts)
         end
     end
isabelle