450 val _ = tracing ("alpha_refl\n" ^ |
450 val _ = tracing ("alpha_refl\n" ^ |
451 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
451 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
452 val _ = tracing ("alpha_bn_imp\n" ^ |
452 val _ = tracing ("alpha_bn_imp\n" ^ |
453 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) |
453 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) |
454 |
454 |
|
455 (* old stuff *) |
455 val _ = |
456 val _ = |
456 if get_STEPS lthy > 13 |
457 if get_STEPS lthy > 13 |
457 then true else raise TEST lthy4 |
458 then true else raise TEST lthy4 |
458 |
459 |
459 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
460 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
460 val bns = raw_bn_funs ~~ bn_nos; |
461 val bns = raw_bn_funs ~~ bn_nos; |
461 |
462 |
462 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
463 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
463 |
464 |
464 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
465 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
|
466 |
|
467 val _ = tracing ("reflps\n" ^ |
|
468 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) reflps)) |
|
469 |
|
470 val _ = |
|
471 if get_STEPS lthy > 13 |
|
472 then true else raise TEST lthy4 |
|
473 |
465 val alpha_equivp = |
474 val alpha_equivp = |
466 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
475 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
467 else build_equivps alpha_trms reflps alpha_induct |
476 else build_equivps alpha_trms reflps alpha_induct |
468 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
477 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
469 |
478 |