src/Pure/thm.ML
changeset 4589 543e867efe40
parent 4439 02730662e446
child 4667 6328d427a339
     1.1 --- a/src/Pure/thm.ML	Fri Jan 30 11:32:19 1998 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Jan 30 11:33:01 1998 +0100
     1.3 @@ -1800,14 +1800,17 @@
     1.4                             prop = prop',
     1.5                             maxidx = maxidx'}
     1.6              val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
     1.7 -        in if perm andalso not(termless(rhs',lhs')) then None else
     1.8 -           if unconditional
     1.9 -           then (trace_thm false "Rewriting:" thm'; 
    1.10 -                 Some(shyps', hyps', rhs', der'::ders))
    1.11 -           else (trace_thm false "Trying to rewrite:" thm';
    1.12 -                 case prover mss thm' of
    1.13 -                   None       => (trace_thm false "FAILED" thm'; None)
    1.14 -                 | Some(thm2) => check_conv(thm2,prop',ders))
    1.15 +        in
    1.16 +          if perm andalso not(termless(rhs',lhs')) then None
    1.17 +          else
    1.18 +           (trace_thm false "Applying instance of rewrite rule:" thm;
    1.19 +            if unconditional
    1.20 +            then (trace_thm false "Rewriting:" thm'; 
    1.21 +                  Some(shyps', hyps', rhs', der'::ders))
    1.22 +            else (trace_thm false "Trying to rewrite:" thm';
    1.23 +                  case prover mss thm' of
    1.24 +                    None       => (trace_thm false "FAILED" thm'; None)
    1.25 +                  | Some(thm2) => check_conv(thm2,prop',ders)))
    1.26          end
    1.27  
    1.28        fun rews [] = None