src/HOL/Library/cconv.ML
changeset 60048 e9c30726ca8e
parent 59975 da10875adf8e
child 60049 e4a5dfee0f9c
     1.1 --- a/src/HOL/Library/cconv.ML	Mon Apr 13 10:21:35 2015 +0200
     1.2 +++ b/src/HOL/Library/cconv.ML	Mon Apr 13 10:39:49 2015 +0200
     1.3 @@ -95,10 +95,11 @@
     1.4      val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1
     1.5      val rule3 = Thm.instantiate (Thm.match (lhs, ct)) rule2
     1.6                  handle Pattern.MATCH => raise CTERM ("rewr_cconv", [lhs, ct])
     1.7 +    val concl = rule3 |> Thm.cprop_of |> Drule.strip_imp_concl
     1.8      val rule4 =
     1.9 -      if concl_lhs_of rule3 aconvc ct then rule3
    1.10 -      else let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
    1.11 -           in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (concl_rhs_of rule3)) end
    1.12 +      if Thm.dest_equals_lhs concl aconvc ct then rule3
    1.13 +      else let val ceq = Thm.dest_fun2 concl
    1.14 +           in rule3 RS Thm.trivial (Thm.mk_binop ceq ct (Thm.dest_equals_rhs concl)) end
    1.15    in
    1.16      transitive rule4 (Thm.beta_conversion true (concl_rhs_of rule4))
    1.17    end