--- 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