diff -r f4599af94b83 -r 0c7f90147f5d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue May 23 09:08:18 2000 +0200
+++ b/src/Provers/classical.ML	Tue May 23 12:13:45 2000 +0200
@@ -325,17 +325,17 @@
   is still allowed.*)
 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
        if mem_thm (th, safeIs) then 
-	 warning ("Rule already in claset as Safe Intr\n" ^ string_of_thm th)
+	 warning ("Rule already declared as safe introduction (intro)\n" ^ string_of_thm th)
   else if mem_thm (th, safeEs) then
-         warning ("Rule already in claset as Safe Elim\n" ^ string_of_thm th)
+         warning ("Rule already declared as safe elimination (elim)\n" ^ string_of_thm th)
   else if mem_thm (th, hazIs) then 
-         warning ("Rule already in claset as unsafe Intr\n" ^ string_of_thm th)
+         warning ("Rule already declared as unsafe introduction (intro?)\n" ^ string_of_thm th)
   else if mem_thm (th, hazEs) then 
-         warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th)
+         warning ("Rule already declared as unsafe elimination (elim?)\n" ^ string_of_thm th)
   else if mem_thm (th, xtraIs) then 
-         warning ("Rule already in claset as extra Intr\n" ^ string_of_thm th)
+         warning ("Rule already declared as extra introduction (intro??)\n" ^ string_of_thm th)
   else if mem_thm (th, xtraEs) then 
-         warning ("Rule already in claset as extra Elim\n" ^ string_of_thm th)
+         warning ("Rule already declared as extra elimination (elim??)\n" ^ string_of_thm th)
   else ();
 
 (*** Safe rules ***)
@@ -653,7 +653,7 @@
 	  mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
           mem_thm (th, xtraIs)  orelse mem_thm (th, xtraEs) 
        then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs)))))
-       else (warning ("Rule not in claset\n" ^ (string_of_thm th)); 
+       else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); 
 	     cs);
 
 val op delrules = foldl delrule;