# HG changeset patch
# User wenzelm
# Date 886156381 -3600
# Node ID 543e867efe40399fe893cba7f60c824aaeeae093
# Parent  42bf47c1de1f81e8404eaa8f877321757308ea93
improved tracing of rewrite rule application;

diff -r 42bf47c1de1f -r 543e867efe40 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jan 30 11:32:19 1998 +0100
+++ b/src/Pure/thm.ML	Fri Jan 30 11:33:01 1998 +0100
@@ -1800,14 +1800,17 @@
                            prop = prop',
                            maxidx = maxidx'}
             val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
-        in if perm andalso not(termless(rhs',lhs')) then None else
-           if unconditional
-           then (trace_thm false "Rewriting:" thm'; 
-                 Some(shyps', hyps', rhs', der'::ders))
-           else (trace_thm false "Trying to rewrite:" thm';
-                 case prover mss thm' of
-                   None       => (trace_thm false "FAILED" thm'; None)
-                 | Some(thm2) => check_conv(thm2,prop',ders))
+        in
+          if perm andalso not(termless(rhs',lhs')) then None
+          else
+           (trace_thm false "Applying instance of rewrite rule:" thm;
+            if unconditional
+            then (trace_thm false "Rewriting:" thm'; 
+                  Some(shyps', hyps', rhs', der'::ders))
+            else (trace_thm false "Trying to rewrite:" thm';
+                  case prover mss thm' of
+                    None       => (trace_thm false "FAILED" thm'; None)
+                  | Some(thm2) => check_conv(thm2,prop',ders)))
         end
 
       fun rews [] = None