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