# HG changeset patch
# User kuncar
# Date 1368612818 -7200
# Node ID 26aecb553c7432a6bf9f1ae80cbd203b759075ce
# Parent  07344a4f19db574726851fc55830927b6661c3dd
abstract equalities only in a correspondence relation in a transfer domain rule

diff -r 07344a4f19db -r 26aecb553c74 src/HOL/Tools/transfer.ML
--- 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