1.1 --- a/src/Pure/Isar/class.ML	Tue Apr 03 10:04:41 2012 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Apr 03 10:59:20 2012 +0200
     1.3 @@ -553,9 +553,7 @@
     1.4      |> Local_Theory.init naming
     1.5         {define = Generic_Target.define foundation,
     1.6          notes = Generic_Target.notes Generic_Target.theory_notes,
     1.7 -        abbrev = Generic_Target.abbrev
     1.8 -          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
     1.9 -            Generic_Target.theory_abbrev prmode ((b, mx), t)),
    1.10 +        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
    1.11          declaration = K Generic_Target.theory_declaration,
    1.12          pretty = pretty,
    1.13          exit = Local_Theory.target_of o conclude}

     2.1 --- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 10:04:41 2012 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 10:59:20 2012 +0200
     2.3 @@ -38,7 +38,8 @@
     2.4      (Attrib.binding * (thm list * Args.src list) list) list ->
     2.5      (Attrib.binding * (thm list * Args.src list) list) list ->
     2.6      local_theory -> local_theory
     2.7 -  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
     2.8 +  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
     2.9 +    local_theory -> local_theory
    2.10    val theory_declaration: declaration -> local_theory -> local_theory
    2.11  end
    2.12  
    2.13 @@ -300,10 +301,13 @@
    2.14        ctxt |> Attrib.local_notes kind
    2.15          (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
    2.16  
    2.17 -fun theory_abbrev prmode ((b, mx), t) =
    2.18 -  Local_Theory.background_theory
    2.19 +fun theory_abbrev prmode (b, mx) (t, _) xs =
    2.20 +  Local_Theory.background_theory_result
    2.21      (Sign.add_abbrev (#1 prmode) (b, t) #->
    2.22 -      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
    2.23 +      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)] #> pair lhs))
    2.24 +  #-> (fn lhs => fn lthy' => lthy' |>
    2.25 +        const_declaration (fn level => level <> Local_Theory.level lthy') prmode
    2.26 +          ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
    2.27  
    2.28  fun theory_declaration decl =
    2.29    background_declaration decl #> standard_declaration (K true) decl;

     3.1 --- a/src/Pure/Isar/named_target.ML	Tue Apr 03 10:04:41 2012 +0200
     3.2 +++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 10:59:20 2012 +0200
     3.3 @@ -100,18 +100,15 @@
     3.4  fun locale_abbrev ta prmode ((b, mx), t) xs =
     3.5    Local_Theory.background_theory_result
     3.6      (Sign.add_abbrev Print_Mode.internal (b, t)) #->
     3.7 -      (fn (lhs, _) => locale_const ta prmode
     3.8 -        ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
     3.9 +      (fn (lhs, _) =>
    3.10 +        locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
    3.11  
    3.12 -fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
    3.13 -    prmode (b, mx) (global_rhs, t') xs lthy =
    3.14 +fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy =
    3.15    if is_locale then
    3.16      lthy
    3.17 -    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
    3.18 +    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs
    3.19      |> is_class ? Class.abbrev target prmode ((b, mx), t')
    3.20 -  else
    3.21 -    lthy
    3.22 -    |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
    3.23 +  else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs;
    3.24  
    3.25  
    3.26  (* declaration *)

     4.1 --- a/src/Pure/Isar/overloading.ML	Tue Apr 03 10:04:41 2012 +0200
     4.2 +++ b/src/Pure/Isar/overloading.ML	Tue Apr 03 10:59:20 2012 +0200
     4.3 @@ -204,9 +204,7 @@
     4.4      |> Local_Theory.init naming
     4.5         {define = Generic_Target.define foundation,
     4.6          notes = Generic_Target.notes Generic_Target.theory_notes,
     4.7 -        abbrev = Generic_Target.abbrev
     4.8 -          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
     4.9 -            Generic_Target.theory_abbrev prmode ((b, mx), t)),
    4.10 +        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
    4.11          declaration = K Generic_Target.theory_declaration,
    4.12          pretty = pretty,
    4.13          exit = Local_Theory.target_of o conclude}