self-contained formulation of abbrev for named targets

--- a/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -18,7 +18,7 @@
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
   val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
-  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> term -> term list * term list -> local_theory -> local_theory
+  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
   val class_prefix: string -> string
   val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -413,7 +413,7 @@
     |> synchronize_class_syntax_target class
   end;
 
-fun abbrev class prmode ((b, mx), lhs) rhs' params lthy =
+fun target_abbrev class prmode ((b, mx), lhs) rhs' params lthy =
   let
     val phi = morphism (Proof_Context.theory_of lthy) class;
     val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
@@ -427,6 +427,10 @@
     |> synchronize_class_syntax_target class
   end;
 
+fun abbrev class = Generic_Target.abbrev (fn prmode => fn (b, mx) => fn global_rhs => fn params =>
+  Generic_Target.background_abbrev (b, global_rhs) (snd params)
+  #-> (fn (lhs, rhs) => target_abbrev class prmode ((b, mx), lhs) rhs params));
+
 end;
 
 

--- a/src/Pure/Isar/generic_target.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -42,6 +42,8 @@
     local_theory -> local_theory
 
   (*theory target operations*)
+  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> (term * term) * local_theory
   val theory_declaration: declaration -> local_theory -> local_theory
   val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
@@ -51,11 +53,15 @@
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
+  val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+    local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
 
   (*locale operations*)
+  val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> (term * term) * local_theory
   val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
     local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
@@ -333,6 +339,8 @@
 
 (** theory operations **)
 
+val theory_abbrev = abbrev theory_target_abbrev;
+
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
 
@@ -375,4 +383,13 @@
   (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
   #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
 
+
+(** locale abbreviations **)
+
+fun locale_target_abbrev locale prmode (b, mx) global_rhs params =
+  background_abbrev (b, global_rhs) (snd params)
+  #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs));
+
+fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
+
 end;

--- a/src/Pure/Isar/named_target.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -88,17 +88,9 @@
 
 (* abbrev *)
 
-fun locale_abbrev locale prmode (b, mx) global_rhs params =
-  Generic_Target.background_abbrev (b, global_rhs) (snd params)
-  #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
-
-fun class_abbrev class prmode (b, mx) global_rhs params =
-  Generic_Target.background_abbrev (b, global_rhs) (snd params)
-  #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params);
-
-fun abbrev ("", _) = Generic_Target.theory_target_abbrev
-  | abbrev (locale, false) = locale_abbrev locale
-  | abbrev (class, true) = class_abbrev class;
+fun abbrev ("", _) = Generic_Target.theory_abbrev
+  | abbrev (locale, false) = Generic_Target.locale_abbrev locale
+  | abbrev (class, true) = Class.abbrev class;
 
 
 (* declaration *)
@@ -165,7 +157,7 @@
     |> Local_Theory.init background_naming
        {define = Generic_Target.define (foundation name_data),
         notes = Generic_Target.notes (notes name_data),
-        abbrev = Generic_Target.abbrev (abbrev name_data),
+        abbrev = abbrev name_data,
         declaration = declaration name_data,
         subscription = subscription name_data,
         pretty = pretty name_data,