src/Tools/induct.ML
changeset 32861 105f40051387
parent 32432 64f30bdd3ba1
child 33303 1e1210f31207
     1.1 --- a/src/Tools/induct.ML	Fri Oct 02 22:02:54 2009 +0200
     1.2 +++ b/src/Tools/induct.ML	Fri Oct 02 22:15:08 2009 +0200
     1.3 @@ -505,7 +505,6 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      val cert = Thm.cterm_of thy;
     1.7 -    val certT = Thm.ctyp_of thy;
     1.8  
     1.9      val v = Free (x, T);
    1.10      fun spec_rule prfx (xs, body) =
    1.11 @@ -579,7 +578,6 @@
    1.12  fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
    1.13    let
    1.14      val thy = ProofContext.theory_of ctxt;
    1.15 -    val cert = Thm.cterm_of thy;
    1.16  
    1.17      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    1.18      val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
    1.19 @@ -652,7 +650,6 @@
    1.20  fun coinduct_tac ctxt inst taking opt_rule facts =
    1.21    let
    1.22      val thy = ProofContext.theory_of ctxt;
    1.23 -    val cert = Thm.cterm_of thy;
    1.24  
    1.25      fun inst_rule r =
    1.26        if null inst then `RuleCases.get r