# HG changeset patch
# User haftmann
# Date 1402263051 -7200
# Node ID d59c4383cae45ccdcf094ffc3e028ddd665a8783
# Parent  180e955711cf8c4607bf16738c1bce36cf1edb85
self-contained locale_declaration operation

diff -r 180e955711cf -r d59c4383cae4 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Jun 08 23:30:51 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Jun 08 23:30:51 2014 +0200
@@ -7,9 +7,6 @@
 
 signature GENERIC_TARGET =
 sig
-  (* declarations *)
-  val standard_declaration: (int * int -> bool) -> declaration -> local_theory -> local_theory
-
   (* consts *)
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
@@ -53,6 +50,8 @@
     (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
+    local_theory -> local_theory
   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
@@ -345,6 +344,11 @@
     Locale.add_declaration locale syntax
       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
 
+fun locale_declaration locale {syntax, pervasive} decl =
+  pervasive ? background_declaration decl
+  #> locale_target_declaration locale syntax decl
+  #> standard_declaration (fn (_, other) => other <> 0) decl;
+
 fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
   locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
 
diff -r 180e955711cf -r d59c4383cae4 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Jun 08 23:30:51 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Jun 08 23:30:51 2014 +0200
@@ -71,7 +71,7 @@
   #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
     #> pair (lhs, def));
 
-fun foundation (ta as Target {target, is_locale, is_class, ...}) =
+fun foundation (Target {target, is_locale, is_class, ...}) =
   if is_class then class_foundation target
   else if is_locale then locale_foundation target
   else Generic_Target.theory_foundation;
@@ -94,7 +94,7 @@
   Generic_Target.background_abbrev (b, global_rhs) (snd params)
   #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params);
 
-fun abbrev (ta as Target {target, is_locale, is_class, ...}) =
+fun abbrev (Target {target, is_locale, is_class, ...}) =
   if is_class then class_abbrev target
   else if is_locale then locale_abbrev target
   else Generic_Target.theory_abbrev;
@@ -102,11 +102,8 @@
 
 (* declaration *)
 
-fun declaration (Target {target, is_locale, ...}) {syntax, pervasive} decl =
-  if is_locale then
-    pervasive ? Generic_Target.background_declaration decl
-    #> Generic_Target.locale_target_declaration target syntax decl
-    #> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl
+fun declaration (Target {target, is_locale, ...}) flags decl =
+  if is_locale then Generic_Target.locale_declaration target flags decl
   else Generic_Target.theory_declaration decl;