# HG changeset patch
# User haftmann
# Date 1401297498 -7200
# Node ID 95e5a633a18f90c6093c402133b0948024a10bf1
# Parent  84c1e0453bda3be964dc744bb365122a95d2c059
uniform treatmen of result

diff -r 84c1e0453bda -r 95e5a633a18f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed May 28 19:17:32 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed May 28 19:18:18 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), rhs))
+  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, params), Logic.unvarify_global rhs))
 
 fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let