equal
deleted
inserted
replaced
134 end; |
134 end; |
135 |
135 |
136 type inductive_info = |
136 type inductive_info = |
137 {names: string list, coind: bool} * inductive_result; |
137 {names: string list, coind: bool} * inductive_result; |
138 |
138 |
139 structure InductiveData = GenericDataFun |
139 structure InductiveData = Generic_Data |
140 ( |
140 ( |
141 type T = inductive_info Symtab.table * thm list; |
141 type T = inductive_info Symtab.table * thm list; |
142 val empty = (Symtab.empty, []); |
142 val empty = (Symtab.empty, []); |
143 val extend = I; |
143 val extend = I; |
144 fun merge _ ((tab1, monos1), (tab2, monos2)) = |
144 fun merge ((tab1, monos1), (tab2, monos2)) : T = |
145 (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2)); |
145 (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2)); |
146 ); |
146 ); |
147 |
147 |
148 val get_inductives = InductiveData.get o Context.Proof; |
148 val get_inductives = InductiveData.get o Context.Proof; |
149 |
149 |