# HG changeset patch
# User wenzelm
# Date 1254514530 -7200
# Node ID 1fc86cec3bdf2be14e05a656934f25a3fb305b82
# Parent  105f4005138793b184fbb658d423655d7e896b5f
eliminated dead code and redundant parameters;
tuned;

diff -r 105f40051387 -r 1fc86cec3bdf src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Oct 02 22:15:08 2009 +0200
+++ b/src/Provers/classical.ML	Fri Oct 02 22:15:30 2009 +0200
@@ -696,13 +696,13 @@
 
 (*Backtracking is allowed among the various these unsafe ways of
   proving a subgoal.  *)
-fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
-  assume_tac                      APPEND'
-  contr_tac                       APPEND'
+fun inst0_step_tac (CS {safe0_netpair, ...}) =
+  assume_tac APPEND'
+  contr_tac APPEND'
   biresolve_from_nets_tac safe0_netpair;
 
 (*These unsafe steps could generate more subgoals.*)
-fun instp_step_tac (CS{safep_netpair,...}) =
+fun instp_step_tac (CS {safep_netpair, ...}) =
   biresolve_from_nets_tac safep_netpair;
 
 (*These steps could instantiate variables and are therefore unsafe.*)
@@ -910,7 +910,6 @@
 val introN = "intro";
 val elimN = "elim";
 val destN = "dest";
-val ruleN = "rule";
 
 val setup_attrs =
   Attrib.setup @{binding swapped} (Scan.succeed swapped)