src/CCL/Wfd.thy
changeset 20193 46f5ef758422
parent 20140 98acc6d0fab6
child 22846 fb79144af9a3
--- a/src/CCL/Wfd.thy	Tue Jul 25 16:51:26 2006 +0200
+++ b/src/CCL/Wfd.thy	Tue Jul 25 21:17:58 2006 +0200
@@ -504,7 +504,7 @@
   type T = thm list;
   val empty = [];
   val extend = I;
-  fun merge _ (rules1, rules2) = gen_union Drule.eq_thm_prop (rules1, rules2);
+  fun merge _ = Drule.merge_rules;
   fun print _ _ = ();
 );