equal
deleted
inserted
replaced
210 prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3; |
210 prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3; |
211 |
211 |
212 val ([size_thms], thy'') = PureThy.add_thmss |
212 val ([size_thms], thy'') = PureThy.add_thmss |
213 [(("size", size_eqns), |
213 [(("size", size_eqns), |
214 [Simplifier.simp_add, Thm.declaration_attribute |
214 [Simplifier.simp_add, Thm.declaration_attribute |
215 (fn thm => Context.mapping (Code.add_default_func thm) I)])] thy' |
215 (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy' |
216 |
216 |
217 in |
217 in |
218 SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms)) |
218 SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms)) |
219 (new_type_names ~~ size_names)) thy'' |
219 (new_type_names ~~ size_names)) thy'' |
220 end; |
220 end; |