diff -r 063698416239 -r a40369ea3ba5 src/Pure/Isar/generic_target.ML
--- 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;