| 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 _ _ = (); );