diff -r 16481a4cc9f3 -r 66925f23ac7f src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu May 10 13:44:44 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu May 10 17:28:40 2001 +0200
@@ -584,7 +584,9 @@
         val unconditional = (Logic.count_prems (prop',0) = 0);
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
       in
-        if perm andalso not (termless (rhs', lhs')) then None
+        if perm andalso not (termless (rhs', lhs'))
+        then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
+              trace_thm false "Term does not become smaller:" thm'; None)
         else
           (trace_thm false "Applying instance of rewrite rule:" thm;
            if unconditional