eliminated dead code and redundant parameters;
authorwenzelm
Fri Oct 02 22:15:30 2009 +0200 (2009-10-02)
changeset 328621fc86cec3bdf
parent 32861 105f40051387
child 32863 5e8cef567042
eliminated dead code and redundant parameters;
tuned;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Fri Oct 02 22:15:08 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Oct 02 22:15:30 2009 +0200
     1.3 @@ -696,13 +696,13 @@
     1.4  
     1.5  (*Backtracking is allowed among the various these unsafe ways of
     1.6    proving a subgoal.  *)
     1.7 -fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
     1.8 -  assume_tac                      APPEND'
     1.9 -  contr_tac                       APPEND'
    1.10 +fun inst0_step_tac (CS {safe0_netpair, ...}) =
    1.11 +  assume_tac APPEND'
    1.12 +  contr_tac APPEND'
    1.13    biresolve_from_nets_tac safe0_netpair;
    1.14  
    1.15  (*These unsafe steps could generate more subgoals.*)
    1.16 -fun instp_step_tac (CS{safep_netpair,...}) =
    1.17 +fun instp_step_tac (CS {safep_netpair, ...}) =
    1.18    biresolve_from_nets_tac safep_netpair;
    1.19  
    1.20  (*These steps could instantiate variables and are therefore unsafe.*)
    1.21 @@ -910,7 +910,6 @@
    1.22  val introN = "intro";
    1.23  val elimN = "elim";
    1.24  val destN = "dest";
    1.25 -val ruleN = "rule";
    1.26  
    1.27  val setup_attrs =
    1.28    Attrib.setup @{binding swapped} (Scan.succeed swapped)