# HG changeset patch
# User oheimb
# Date 888434998 -3600
# Node ID d60f76680bf4fdaa9cd1a074f15bef61e41e07a8
# Parent  d24cca140eebbf71f5ae476b4ab732bebcf42344
renamed rep_claset to rep_cs

diff -r d24cca140eeb -r d60f76680bf4 src/FOL/cladata.ML
--- 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);
diff -r d24cca140eeb -r d60f76680bf4 src/FOLP/classical.ML
--- 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. *)
diff -r d24cca140eeb -r d60f76680bf4 src/HOL/cladata.ML
--- 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);
diff -r d24cca140eeb -r d60f76680bf4 src/Provers/blast.ML
--- 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, []) = 
diff -r d24cca140eeb -r d60f76680bf4 src/Provers/classical.ML
--- 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);