187 mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn)) |
187 mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn)) |
188 (args, Datatype_Prop.make_tnames (map third args))); |
188 (args, Datatype_Prop.make_tnames (map third args))); |
189 val eqs : eq list = |
189 val eqs : eq list = |
190 map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; |
190 map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; |
191 |
191 |
192 val ((rewss, take_rews), theorems_thy) = |
192 val (constr_infos, thy) = |
193 thy |
193 thy |
194 |> fold_map (fn (((dbind, eq), (_,cs)), info) => |
194 |> fold_map (fn ((dbind, (_,cs)), info) => |
195 Domain_Theorems.theorems (eq, eqs) dbind cs info take_info) |
195 Domain_Constructors.add_domain_constructors dbind cs info) |
196 (dbinds ~~ eqs ~~ eqs' ~~ iso_infos) |
196 (dbinds ~~ eqs' ~~ iso_infos); |
197 ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info; |
197 |
|
198 val (take_rews, theorems_thy) = |
|
199 thy |
|
200 |> Domain_Theorems.comp_theorems (comp_dbind, eqs) |
|
201 (dbinds ~~ map snd eqs') iso_infos take_info constr_infos; |
198 in |
202 in |
199 theorems_thy |
203 theorems_thy |
200 |> Global_Theory.add_thmss |
|
201 [((Binding.qualified true "rews" comp_dbind, |
|
202 flat rewss @ take_rews), [])] |
|
203 |> snd |
|
204 end; |
204 end; |
205 |
205 |
206 fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = |
206 fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = |
207 let |
207 let |
208 fun prep (dbind, mx, (lhsT, rhsT)) = |
208 fun prep (dbind, mx, (lhsT, rhsT)) = |