--- a/src/FOL/cladata.ML Wed Feb 25 20:25:27 1998 +0100
+++ b/src/FOL/cladata.ML Wed Feb 25 20:29:58 1998 +0100
@@ -56,7 +56,7 @@
val dup_intr = Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset = Cla.claset
- val rep_claset = Cla.rep_claset
+ val rep_cs = Cla.rep_cs
end;
structure Blast = BlastFun(Blast_Data);
--- a/src/FOLP/classical.ML Wed Feb 25 20:25:27 1998 +0100
+++ b/src/FOLP/classical.ML Wed Feb 25 20:29:58 1998 +0100
@@ -41,7 +41,7 @@
val addSEs: claset * thm list -> claset
val addSIs: claset * thm list -> claset
val print_cs: claset -> unit
- val rep_claset: claset ->
+ val rep_cs: claset ->
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list,
safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
haz_brls: (bool*thm)list}
@@ -102,7 +102,7 @@
safep_brls: (bool*thm)list,
haz_brls: (bool*thm)list};
-fun rep_claset (CS x) = x;
+fun rep_cs (CS x) = x;
(*For use with biresolve_tac. Combines intrs with swap to catch negated
assumptions. Also pairs elims with true. *)
--- a/src/HOL/cladata.ML Wed Feb 25 20:25:27 1998 +0100
+++ b/src/HOL/cladata.ML Wed Feb 25 20:29:58 1998 +0100
@@ -75,7 +75,7 @@
val dup_intr = Classical.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset = Classical.claset
- val rep_claset = Classical.rep_claset
+ val rep_cs = Classical.rep_cs
end;
structure Blast = BlastFun(Blast_Data);
--- a/src/Provers/blast.ML Wed Feb 25 20:25:27 1998 +0100
+++ b/src/Provers/blast.ML Wed Feb 25 20:29:58 1998 +0100
@@ -61,7 +61,7 @@
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,
@@ -918,7 +918,7 @@
"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, []) =
--- a/src/Provers/classical.ML Wed Feb 25 20:25:27 1998 +0100
+++ b/src/Provers/classical.ML Wed Feb 25 20:29:58 1998 +0100
@@ -49,7 +49,7 @@
val empty_cs: claset
val print_cs: claset -> unit
val print_claset: theory -> unit
- val rep_claset: (* BLAST_DATA in blast.ML dependent on this *)
+ val rep_cs: (* BLAST_DATA in blast.ML dependent on this *)
claset -> {safeIs: thm list, safeEs: thm list,
hazIs: thm list, hazEs: thm list,
swrappers: (string * wrapper) list,
@@ -260,7 +260,7 @@
Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs))
end;
-fun rep_claset (CS args) = args;
+fun rep_cs (CS args) = args;
local
fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac);