src/Provers/classical.ML

 
 (*** Unsafe steps instantiate variables or lose information ***)
 
 (*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.*)
 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
 

 (** concrete syntax of attributes **)
 
 val introN = "intro";
 val elimN = "elim";
 val destN = "dest";
-val ruleN = "rule";
 
 val setup_attrs =
   Attrib.setup @{binding swapped} (Scan.succeed swapped)
     "classical swap of introduction rule" #>
   Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)