# HG changeset patch
# User haftmann
# Date 1400773981 -7200
# Node ID 9c990475d44f2c4e53150ddfe45f2602ab1e9641
# Parent  dfac6ef0ca2809d696856f247b4423c32dbc6b71
tuned signature

diff -r dfac6ef0ca28 -r 9c990475d44f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 22 17:53:01 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 22 17:53:01 2014 +0200
@@ -20,7 +20,7 @@
     (Attrib.binding * (thm list * Args.src list) list) list ->
     (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
-  val background_abbrev: binding * term -> local_theory -> (term * term) * local_theory
+  val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
   val abbrev: (string * bool -> binding * mixfix -> term * term ->
       term list -> local_theory -> local_theory) ->
     string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
@@ -198,8 +198,9 @@
 
 (* abbrev *)
 
-fun background_abbrev (b, t) =
+fun background_abbrev (b, t) xs =
   Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t))
+  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, xs), rhs))
 
 fun abbrev target_abbrev prmode ((b, mx), t) lthy =
   let
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