src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58203 9003cc8ac94d
parent 58180 95397823f39e
child 58340 5f6f48e87de6
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sun Sep 07 17:51:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 08 09:52:06 2014 +0200
     1.3 @@ -182,12 +182,14 @@
     1.4      val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
     1.5      val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
     1.6  
     1.7 +    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
     1.8 +
     1.9      val rel_xtor_co_induct_thm =
    1.10 -      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors
    1.11 -        xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
    1.12 +      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.13 +        xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    1.14 +          rel_monos rel_eqs)
    1.15          lthy;
    1.16  
    1.17 -    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    1.18      val map_id0s = no_refl (map map_id0_of_bnf bnfs);
    1.19  
    1.20      val xtor_co_induct_thm =