diff -r a4ab5d0cccd1 -r 105f40051387 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Oct 02 22:02:54 2009 +0200
+++ b/src/Tools/induct.ML	Fri Oct 02 22:15:08 2009 +0200
@@ -505,7 +505,6 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
 
     val v = Free (x, T);
     fun spec_rule prfx (xs, body) =
@@ -579,7 +578,6 @@
 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
@@ -652,7 +650,6 @@
 fun coinduct_tac ctxt inst taking opt_rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     fun inst_rule r =
       if null inst then `RuleCases.get r