src/Provers/blast.ML
changeset 4653 d60f76680bf4
parent 4651 70dd492a1698
child 5343 871b77df79a0
     1.1 --- a/src/Provers/blast.ML	Wed Feb 25 20:25:27 1998 +0100
     1.2 +++ b/src/Provers/blast.ML	Wed Feb 25 20:29:58 1998 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4    val dup_intr		: thm -> thm
     1.5    val hyp_subst_tac     : bool ref -> int -> tactic
     1.6    val claset		: unit -> claset
     1.7 -  val rep_claset	: (* dependent on classical.ML *)
     1.8 +  val rep_cs	: (* dependent on classical.ML *)
     1.9        claset -> {safeIs: thm list, safeEs: thm list, 
    1.10  		 hazIs: thm list, hazEs: thm list,
    1.11  		 swrappers: (string * wrapper) list, 
    1.12 @@ -918,7 +918,7 @@
    1.13   "start" is CPU time at start, for printing search time
    1.14  *)
    1.15  fun prove (sign, start, cs, brs, cont) =
    1.16 - let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs
    1.17 + let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
    1.18       val safeList = [safe0_netpair, safep_netpair]
    1.19       and hazList  = [haz_netpair]
    1.20       fun prv (tacs, trs, choices, []) =