# HG changeset patch
# User nipkow
# Date 1426259395 -3600
# Node ID 46b635624feb8f9b15719bd76f1d440fd96d55c5
# Parent  7968c57ea240a42931027193825616be70e744bf
rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

diff -r 7968c57ea240 -r 46b635624feb src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri Mar 13 12:58:49 2015 +0100
+++ b/src/Pure/raw_simplifier.ML	Fri Mar 13 16:09:55 2015 +0100
@@ -845,8 +845,15 @@
 fun check_conv ctxt msg thm thm' =
   let
     val thm'' = Thm.transitive thm thm' handle THM _ =>
-     Thm.transitive thm (Thm.transitive
-       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
+      let
+        val nthm' =
+          Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm'
+      in Thm.transitive thm nthm' handle THM _ =>
+           let
+             val nthm =
+               Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm))
+           in Thm.transitive nthm nthm' end
+      end
     val _ =
       if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
       else ();