eliminated dead code and redundant parameters;
authorwenzelm
Fri, 02 Oct 2009 22:15:30 +0200 (2009-10-02)
changeset 32862 1fc86cec3bdf
parent 32861 105f40051387
child 32863 5e8cef567042
eliminated dead code and redundant parameters; tuned;
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)