# HG changeset patch
# User blanchet
# Date 1367235694 -7200
# Node ID 329c62d9997992413f20c4412397083d6f768d77
# Parent  1461426e2bf1ec979351cf51d9641fb336316169
removed unreferenced thm

diff -r 1461426e2bf1 -r 329c62d99979 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Apr 29 13:40:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Apr 29 13:41:34 2013 +0200
@@ -572,7 +572,6 @@
     val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]}
         else @{thm ordLeq_csum2[OF Card_order_ctwo]};
     val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp});
-    val Asuc_bd_Cnotzero = Asuc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
 
     val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
       [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
@@ -671,7 +670,7 @@
             (K (mk_min_algs_card_of_tac card_cT card_ct
               m suc_bd_worel min_algs_thms in_bd_sums
               sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
-              suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)))
+              suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
           |> Thm.close_derivation;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
diff -r 1461426e2bf1 -r 329c62d99979 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Mon Apr 29 13:40:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Mon Apr 29 13:41:34 2013 +0200
@@ -47,7 +47,7 @@
   val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
-    thm -> thm -> thm -> thm -> thm -> thm -> tactic
+    thm -> thm -> thm -> thm -> thm -> tactic
   val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
   val mk_min_algs_tac: thm -> thm list -> tactic
@@ -286,7 +286,7 @@
   rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
 
 fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
-  suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite Asuc_Cnotzero =
+  suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
   let
     val induct = worel RS
       Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};