diff -r dfac6ef0ca28 -r 9c990475d44f src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu May 22 17:53:01 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 22 17:53:01 2014 +0200
@@ -76,13 +76,12 @@
 (* abbrev *)
 
 fun locale_abbrev target prmode (b, mx) (t, _) xs =
-  Generic_Target.background_abbrev (b, t)
-  #-> (fn (lhs, _) =>
-        Generic_Target.locale_const_declaration target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+  Generic_Target.background_abbrev (b, t) xs
+  #-> (fn (lhs, _) => Generic_Target.locale_const_declaration target prmode ((b, mx), lhs));
 
 fun class_abbrev target prmode (b, mx) (t, t') xs =
-  Generic_Target.background_abbrev (b, t)
-  #-> (fn (lhs, _) => Class.abbrev target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)) t');
+  Generic_Target.background_abbrev (b, t) xs
+  #-> (fn (lhs, _) => Class.abbrev target prmode ((b, mx), lhs) t');
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) =
   if is_class then class_abbrev target