1.1 --- a/src/Pure/conv.ML	Mon Oct 22 22:47:14 2012 +0200
     1.2 +++ b/src/Pure/conv.ML	Wed Oct 24 17:40:56 2012 +0200
     1.3 @@ -154,17 +154,22 @@
     1.4    | _ => raise CTERM ("implies_concl_conv", [ct]));
     1.5  
     1.6  
     1.7 -(* single rewrite step, cf. REWR_CONV in HOL *)
     1.8 -
     1.9 +(* single rewrite step
    1.10 +   beta-normalizes the rhs and takes care that lhs aconv ct *)
    1.11  fun rewr_conv rule ct =
    1.12    let
    1.13      val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
    1.14      val lhs = Thm.lhs_of rule1;
    1.15      val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    1.16 -  in
    1.17 -    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
    1.18 +    val rule3 =
    1.19 +      Thm.instantiate (Thm.match (lhs, ct)) rule2
    1.20        handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
    1.21 -  end;
    1.22 +    val rule4 =
    1.23 +      if term_of(Thm.lhs_of rule3) aconv term_of ct then rule3
    1.24 +      else
    1.25 +        let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
    1.26 +        in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (Thm.rhs_of rule3)) end
    1.27 +  in Thm.transitive rule4 (Thm.beta_conversion true (Thm.rhs_of rule4)) end
    1.28  
    1.29  fun rewrs_conv rules = first_conv (map rewr_conv rules);
    1.30