abstract equalities only in a correspondence relation in a transfer domain rule

--- a/src/HOL/Tools/transfer.ML	Wed May 15 12:10:44 2013 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed May 15 12:13:38 2013 +0200
@@ -193,12 +193,7 @@
         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
         val ((dom, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
       in
-        (x $ y, fn comb' =>
-          let 
-            val (x', y') = dest_comb comb'
-          in
-            Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y'))
-          end)
+        (x, fn x' => Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y)))
       end
   in
     gen_abstract_equalities dest thm