src/Pure/meta_simplifier.ML
changeset 11295 66925f23ac7f
parent 11291 02db0084a695
child 11371 1d5d181b7e28
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu May 10 13:44:44 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu May 10 17:28:40 2001 +0200
     1.3 @@ -584,7 +584,9 @@
     1.4          val unconditional = (Logic.count_prems (prop',0) = 0);
     1.5          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
     1.6        in
     1.7 -        if perm andalso not (termless (rhs', lhs')) then None
     1.8 +        if perm andalso not (termless (rhs', lhs'))
     1.9 +        then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
    1.10 +              trace_thm false "Term does not become smaller:" thm'; None)
    1.11          else
    1.12            (trace_thm false "Applying instance of rewrite rule:" thm;
    1.13             if unconditional