# HG changeset patch
# User haftmann
# Date 1401396380 -7200
# Node ID ae61587eb44ab7f931ea9f49a362a6532d6b33d8
# Parent  f00a299fa522b39812d3ccc0e533132140b3f24d
even more uniform treatment of result after 95e5a633a18f

diff -r f00a299fa522 -r ae61587eb44a src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 29 15:27:49 2014 +0100
+++ b/src/Pure/Isar/generic_target.ML	Thu May 29 22:46:20 2014 +0200
@@ -200,7 +200,7 @@
 
 fun background_abbrev (b, global_rhs) params =
   Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
-  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, params), Logic.unvarify_global rhs))
+  #>> pairself (fn t => Term.list_comb (Logic.unvarify_global t, params))
 
 fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let