# HG changeset patch
# User wenzelm
# Date 1333443560 -7200
# Node ID 392c4cd97e5c663415795ea1f76d64ed3383f588
# Parent  ca4cf5de366c2b099b1793516ce08821f488edea
more uniform theory_abbrev with const_declaration;

diff -r ca4cf5de366c -r 392c4cd97e5c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Apr 03 10:04:41 2012 +0200
+++ b/src/Pure/Isar/class.ML	Tue Apr 03 10:59:20 2012 +0200
@@ -553,9 +553,7 @@
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev
-          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
-            Generic_Target.theory_abbrev prmode ((b, mx), t)),
+        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
diff -r ca4cf5de366c -r 392c4cd97e5c src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 10:04:41 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 10:59:20 2012 +0200
@@ -38,7 +38,8 @@
     (Attrib.binding * (thm list * Args.src list) list) list ->
     (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
-  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
+  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
+    local_theory -> local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
 end
 
@@ -300,10 +301,13 @@
       ctxt |> Attrib.local_notes kind
         (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
 
-fun theory_abbrev prmode ((b, mx), t) =
-  Local_Theory.background_theory
+fun theory_abbrev prmode (b, mx) (t, _) xs =
+  Local_Theory.background_theory_result
     (Sign.add_abbrev (#1 prmode) (b, t) #->
-      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)] #> pair lhs))
+  #-> (fn lhs => fn lthy' => lthy' |>
+        const_declaration (fn level => level <> Local_Theory.level lthy') prmode
+          ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
diff -r ca4cf5de366c -r 392c4cd97e5c src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Apr 03 10:04:41 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 10:59:20 2012 +0200
@@ -100,18 +100,15 @@
 fun locale_abbrev ta prmode ((b, mx), t) xs =
   Local_Theory.background_theory_result
     (Sign.add_abbrev Print_Mode.internal (b, t)) #->
-      (fn (lhs, _) => locale_const ta prmode
-        ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+      (fn (lhs, _) =>
+        locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
-fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
-    prmode (b, mx) (global_rhs, t') xs lthy =
+fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy =
   if is_locale then
     lthy
-    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs
     |> is_class ? Class.abbrev target prmode ((b, mx), t')
-  else
-    lthy
-    |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+  else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs;
 
 
 (* declaration *)
diff -r ca4cf5de366c -r 392c4cd97e5c src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Tue Apr 03 10:04:41 2012 +0200
+++ b/src/Pure/Isar/overloading.ML	Tue Apr 03 10:59:20 2012 +0200
@@ -204,9 +204,7 @@
     |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev
-          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
-            Generic_Target.theory_abbrev prmode ((b, mx), t)),
+        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
         declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}