src/HOL/BNF/Tools/bnf_comp.ML
changeset 51782 84e7225f5ab6
parent 51767 bbcdd8519253
child 51837 087498724486
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -644,8 +644,8 @@
     1.4        map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
     1.5      val in_bd =
     1.6        @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
     1.7 -        @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
     1.8 -          @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
     1.9 +        @{thm cexp_cong2} OF [bd_ordIso, if live = 0 then
    1.10 +          @{thm Card_order_ctwo} else @{thm Card_order_csum},
    1.11              bd_Card_order_of_bnf bnf]];
    1.12  
    1.13      fun mk_tac thm {context = ctxt, prems = _} =