# HG changeset patch
# User wenzelm
# Date 1333286623 -7200
# Node ID 2bbab021c0e6c8e5b8a0d378dbeac8a7b8960bb4
# Parent  ff1770df59b8e5514906d173b6556d9a3429b967
clarified Named_Target.target_declaration: propagate through other levels as well;
tuned signature;

diff -r ff1770df59b8 -r 2bbab021c0e6 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Apr 01 14:29:22 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Apr 01 15:23:43 2012 +0200
@@ -22,6 +22,7 @@
 
   val background_declaration: declaration -> local_theory -> local_theory
   val standard_declaration: declaration -> local_theory -> local_theory
+  val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
 
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
@@ -194,6 +195,11 @@
   (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt =>
     Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
 
+fun locale_declaration locale syntax decl lthy = lthy
+  |> Local_Theory.target (fn ctxt => ctxt |>
+    Locale.add_declaration locale syntax
+      (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
+
 
 
 (** primitive theory operations **)
diff -r ff1770df59b8 -r 2bbab021c0e6 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Apr 01 14:29:22 2012 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Apr 01 15:23:43 2012 +0200
@@ -49,8 +49,7 @@
   (* Storing results *)
   val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
-  val add_declaration: string -> declaration -> Proof.context -> Proof.context
-  val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
+  val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -553,15 +552,22 @@
 
 (* Declarations *)
 
-fun add_declaration loc decl =
+local
+
+fun add_decl loc decl =
   add_thmss loc ""
     [((Binding.conceal Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];
 
-fun add_syntax_declaration loc decl =
-  Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
-  #> add_declaration loc decl;
+in
+
+fun add_declaration loc syntax decl =
+  syntax ?
+    Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+  #> add_decl loc decl;
+
+end;
 
 
 (*** Reasoning about locales ***)
diff -r ff1770df59b8 -r 2bbab021c0e6 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Apr 01 14:29:22 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Apr 01 15:23:43 2012 +0200
@@ -49,30 +49,10 @@
   else error "Not in a named target (global theory, locale, class)";
 
 
-(* generic declarations *)
-
-fun locale_declaration locale syntax decl lthy =
-  let
-    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
-    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
-  in
-    lthy
-    |> Local_Theory.target (add locale locale_decl)
-  end;
+(* consts in locale *)
 
-fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
-  if target = "" then Generic_Target.standard_declaration decl lthy
-  else
-    lthy
-    |> pervasive ? Generic_Target.background_declaration decl
-    |> locale_declaration target syntax decl
-    |> Context.proof_map (Morphism.form decl);
-
-
-(* consts in locales *)
-
-fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
-  locale_declaration target true (fn phi =>
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+  Generic_Target.locale_declaration target true (fn phi =>
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
@@ -157,6 +137,18 @@
     |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
 
 
+(* declaration *)
+
+fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
+  if target = "" then Generic_Target.standard_declaration decl lthy
+  else
+    lthy
+    |> pervasive ? Generic_Target.background_declaration decl
+    |> Generic_Target.locale_declaration target syntax decl
+    |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => ctxt |>
+        level > 0 ? Context.proof_map (Local_Theory.standard_form lthy' ctxt decl)));
+
+
 (* pretty *)
 
 fun pretty (Target {target, is_locale, is_class, ...}) ctxt =