src/Pure/meta_simplifier.ML

         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = #prop (rep_thm thm');
         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
            then
              (trace_thm false "Rewriting:" thm';