changeset 33699 | f33b036ef318 |
parent 33643 | b275f26a638b |
child 34952 | bd7e347eb768 |
--- a/src/HOL/Tools/recdef.ML Sun Nov 15 19:44:16 2009 +0100 +++ b/src/HOL/Tools/recdef.ML Sun Nov 15 19:44:29 2009 +0100 @@ -96,7 +96,7 @@ (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T = (Symtab.merge (K true) (tab1, tab2), mk_hints (Thm.merge_thms (simps1, simps2), - AList.merge (op =) Thm.eq_thm_prop (congs1, congs2), + AList.merge (op =) (K true) (congs1, congs2), Thm.merge_thms (wfs1, wfs2))); );