# HG changeset patch
# User paulson
# Date 906121969 -7200
# Node ID 2df1a9d43e3c6da6f6cce66b0a6a2f7c49a9395d
# Parent  e335c51808accdf96a67d89f70215490331761a3
improved error messages

diff -r e335c51808ac -r 2df1a9d43e3c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Sep 16 10:28:54 1998 +0200
+++ b/src/Pure/thm.ML	Fri Sep 18 14:32:49 1998 +0200
@@ -1749,11 +1749,14 @@
 
 fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
     (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
-  (trace_term false ("Adding simplification procedure " ^ quote name ^ " for:")
+  (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
       (Sign.deref sign_ref) t;
     mk_mss (rules, congs,
       Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
-        handle Net.INSERT => (trace true "Ignored duplicate"; procs),
+        handle Net.INSERT => 
+	    (warning ("Ignoring duplicate simplification procedure \"" 
+	              ^ name ^ "\""); 
+	     procs),
         bounds, prems, mk_rews, termless));
 
 fun add_simproc (mss, (name, lhss, proc, id)) =
@@ -1768,7 +1771,9 @@
     (name, lhs as Cterm {t, ...}, proc, id)) =
   mk_mss (rules, congs,
     Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
-      handle Net.DELETE => (trace true "Simplification procedure not in simpset"; procs),
+      handle Net.DELETE => 
+	  (warning ("Simplification procedure \"" ^ name ^
+		       "\" not in simpset"); procs),
       bounds, prems, mk_rews, termless);
 
 fun del_simproc (mss, (name, lhss, proc, id)) =