src/Provers/blast.ML

   val ccontr		: thm		
   val contr_tac 	: int -> tactic
   val dup_intr		: thm -> thm
   val hyp_subst_tac     : bool ref -> int -> tactic
   val claset		: unit -> claset
-  val rep_claset	: (* dependent on classical.ML *)
+  val rep_cs	: (* dependent on classical.ML *)
       claset -> {safeIs: thm list, safeEs: thm list, 
 		 hazIs: thm list, hazEs: thm list,
 		 swrappers: (string * wrapper) list, 
 		 uwrappers: (string * wrapper) list,
 		 safe0_netpair: netpair, safep_netpair: netpair,

   branch contains a list of unexpanded formulae, a list of literals, and a 
   bound on unsafe expansions.
  "start" is CPU time at start, for printing search time
 *)
 fun prove (sign, start, cs, brs, cont) =
- let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs
+ let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
      val safeList = [safe0_netpair, safep_netpair]
      and hazList  = [haz_netpair]
      fun prv (tacs, trs, choices, []) = 
 	        (printStats (!trace orelse !stats, start, tacs); 
 		 cont (tacs, trs, choices))   (*all branches closed!*)