84 |
84 |
85 (* theory data *) |
85 (* theory data *) |
86 |
86 |
87 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list}; |
87 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list}; |
88 |
88 |
89 structure GlobalRecdefData = TheoryDataFun |
89 structure GlobalRecdefData = Theory_Data |
90 ( |
90 ( |
91 type T = recdef_info Symtab.table * hints; |
91 type T = recdef_info Symtab.table * hints; |
92 val empty = (Symtab.empty, mk_hints ([], [], [])): T; |
92 val empty = (Symtab.empty, mk_hints ([], [], [])): T; |
93 val copy = I; |
|
94 val extend = I; |
93 val extend = I; |
95 fun merge _ |
94 fun merge |
96 ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}), |
95 ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}), |
97 (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T = |
96 (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T = |
98 (Symtab.merge (K true) (tab1, tab2), |
97 (Symtab.merge (K true) (tab1, tab2), |
99 mk_hints (Thm.merge_thms (simps1, simps2), |
98 mk_hints (Thm.merge_thms (simps1, simps2), |
100 AList.merge (op =) Thm.eq_thm (congs1, congs2), |
99 AList.merge (op =) Thm.eq_thm_prop (congs1, congs2), |
101 Thm.merge_thms (wfs1, wfs2))); |
100 Thm.merge_thms (wfs1, wfs2))); |
102 ); |
101 ); |
103 |
102 |
104 val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get; |
103 val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get; |
105 |
104 |