--- a/src/HOL/Tools/recdef.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/recdef.ML Sun Nov 08 18:43:42 2009 +0100
@@ -86,18 +86,17 @@
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
-structure GlobalRecdefData = TheoryDataFun
+structure GlobalRecdefData = Theory_Data
(
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
(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 (congs1, congs2),
+ AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
Thm.merge_thms (wfs1, wfs2)));
);