210 ML {* add_primrec_wrapper *} |
210 ML {* add_primrec_wrapper *} |
211 |
211 |
212 ML {* |
212 ML {* |
213 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
213 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
214 let |
214 let |
215 val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy') = |
215 val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy2) = |
216 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
216 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
217 in |
217 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
218 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy') |
218 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
|
219 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
|
220 val raw_binds_flat = map (map flat) raw_binds; |
|
221 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; |
|
222 |
|
223 in |
|
224 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
219 end |
225 end |
220 *} |
226 *} |
221 |
227 |
222 ML {* |
228 ML {* |
223 (* parsing the datatypes and declaring *) |
229 (* parsing the datatypes and declaring *) |