# HG changeset patch
# User noschinl
# Date 1428914389 -7200
# Node ID e9c30726ca8eacf2101450a6f9953f4e76baac34
# Parent  58e5b16cbd9450aeb26bcaa48924805c4b8fbce4
rewr_cconv: ignore premises when tuning conclusion

diff -r 58e5b16cbd94 -r e9c30726ca8e src/HOL/Library/cconv.ML
--- a/src/HOL/Library/cconv.ML	Mon Apr 13 10:21:35 2015 +0200
+++ b/src/HOL/Library/cconv.ML	Mon Apr 13 10:39:49 2015 +0200
@@ -95,10 +95,11 @@
     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1
     val rule3 = Thm.instantiate (Thm.match (lhs, ct)) rule2
                 handle Pattern.MATCH => raise CTERM ("rewr_cconv", [lhs, ct])
+    val concl = rule3 |> Thm.cprop_of |> Drule.strip_imp_concl
     val rule4 =
-      if concl_lhs_of rule3 aconvc ct then rule3
-      else let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
-           in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (concl_rhs_of rule3)) end
+      if Thm.dest_equals_lhs concl aconvc ct then rule3
+      else let val ceq = Thm.dest_fun2 concl
+           in rule3 RS Thm.trivial (Thm.mk_binop ceq ct (Thm.dest_equals_rhs concl)) end
   in
     transitive rule4 (Thm.beta_conversion true (concl_rhs_of rule4))
   end