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