src/Provers/classical.ML
changeset 4653 d60f76680bf4
parent 4651 70dd492a1698
child 4742 a25bb8a260ae
     1.1 --- a/src/Provers/classical.ML	Wed Feb 25 20:25:27 1998 +0100
     1.2 +++ b/src/Provers/classical.ML	Wed Feb 25 20:29:58 1998 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4    val empty_cs: claset
     1.5    val print_cs: claset -> unit
     1.6    val print_claset: theory -> unit
     1.7 -  val rep_claset: (* BLAST_DATA in blast.ML dependent on this *)
     1.8 +  val rep_cs: (* BLAST_DATA in blast.ML dependent on this *)
     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 @@ -260,7 +260,7 @@
    1.13      Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs))
    1.14    end;
    1.15  
    1.16 -fun rep_claset (CS args) = args;
    1.17 +fun rep_cs (CS args) = args;
    1.18  
    1.19  local 
    1.20    fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac);