# HG changeset patch
# User wenzelm
# Date 1254514508 -7200
# Node ID 105f4005138793b184fbb658d423655d7e896b5f
# Parent  a4ab5d0cccd1b6d914e57777b2ba8047d2be8214
eliminated dead code;

diff -r a4ab5d0cccd1 -r 105f40051387 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Oct 02 22:02:54 2009 +0200
+++ b/src/Provers/clasimp.ML	Fri Oct 02 22:15:08 2009 +0200
@@ -141,7 +141,6 @@
 
 val addXIs = modifier (ContextRules.intro_query NONE);
 val addXEs = modifier (ContextRules.elim_query NONE);
-val addXDs = modifier (ContextRules.dest_query NONE);
 val delXs = modifier ContextRules.rule_del;
 
 in
@@ -266,9 +265,6 @@
   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
 
 
-fun clasimp_method tac =
-  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
-
 fun clasimp_method' tac =
   Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
 
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
diff -r a4ab5d0cccd1 -r 105f40051387 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Fri Oct 02 22:02:54 2009 +0200
+++ b/src/Tools/intuitionistic.ML	Fri Oct 02 22:15:08 2009 +0200
@@ -69,7 +69,6 @@
 val introN = "intro";
 val elimN = "elim";
 val destN = "dest";
-val ruleN = "rule";
 
 fun modifier name kind kind' att =
   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)