# HG changeset patch
# User nipkow
# Date 989442566 -7200
# Node ID 02db0084a695b923f1ba7c7a98ba27c0e3b0ae93
# Parent  c6a4100d1cd061961a866449e9579f4b7f695d32
improved simproc trace IGNORED

diff -r c6a4100d1cd0 -r 02db0084a695 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue May 08 16:01:36 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Wed May 09 23:09:26 2001 +0200
@@ -630,7 +630,7 @@
              | Some raw_thm =>
                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
                   (case rews (mk_procrule raw_thm) of
-                    None => (trace false "IGNORED"; proc_rews ps)
+                    None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
                   | some => some)))
           else proc_rews ps;
   in case eta_t of