275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
277 val thy = Local_Theory.exit_global lthy2; |
277 val thy = Local_Theory.exit_global lthy2; |
278 val lthy3 = Theory_Target.init NONE thy; |
278 val lthy3 = Theory_Target.init NONE thy; |
279 |
279 |
280 val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
280 val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
281 val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4; |
281 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) = |
|
282 define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4; |
282 in |
283 in |
283 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5) |
284 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5) |
284 end |
285 end |
285 *} |
286 *} |
286 |
287 |