rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

--- 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 ();