# HG changeset patch
# User wenzelm
# Date 959076825 -7200
# Node ID 0c7f90147f5da05a3d7826ff7737a6c2caed3f2d
# Parent  f4599af94b834ac471da16729dfd069cf5eb8d87
improved warning messages;

diff -r f4599af94b83 -r 0c7f90147f5d doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Tue May 23 09:08:18 2000 +0200
+++ b/doc-src/Ref/classical.tex	Tue May 23 12:13:45 2000 +0200
@@ -257,7 +257,7 @@
 delrules : claset * thm list -> claset                 \hfill{\bf infix 4}
 \end{ttbox}
 The add operations ignore any rule already present in the claset with the same
-classification (such as Safe Introduction).  They print a warning if the rule
+classification (such as safe introduction).  They print a warning if the rule
 has already been added with some other classification, but add the rule
 anyway.  Calling \texttt{delrules} deletes all occurrences of a rule from the
 claset, but see the warning below concerning destruction rules.
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;