refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;

--- a/NEWS	Fri Oct 28 23:10:44 2011 +0200
+++ b/NEWS	Fri Oct 28 23:16:50 2011 +0200
@@ -80,6 +80,10 @@
 * Structure Proof_Context follows standard naming scheme.  Old
 ProofContext has been discontinued.  INCOMPATIBILITY.
 
+* Refined Local_Theory.declaration {syntax, pervasive}, with subtle
+change of semantics for syntax = false: update is applied to auxiliary
+context as well.
+
 
 
 New in Isabelle2011-1 (October 2011)

--- a/src/Pure/Isar/class.ML	Fri Oct 28 23:10:44 2011 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 28 23:16:50 2011 +0200
@@ -560,7 +560,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = Generic_Target.theory_declaration o #syntax,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;

--- a/src/Pure/Isar/generic_target.ML	Fri Oct 28 23:10:44 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Oct 28 23:16:50 2011 +0200
@@ -20,7 +20,7 @@
     string * bool -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
 
-  val theory_declaration: declaration -> local_theory -> local_theory
+  val theory_declaration: bool -> declaration -> local_theory -> local_theory
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
@@ -185,7 +185,7 @@
 
 (** primitive theory operations **)
 
-fun theory_declaration decl lthy =
+fun theory_declaration syntax decl lthy =
   let
     val global_decl = Morphism.form
       (Morphism.transform (Local_Theory.global_morphism lthy) decl);
@@ -193,6 +193,7 @@
     lthy
     |> Local_Theory.background_theory (Context.theory_map global_decl)
     |> Local_Theory.target (Context.proof_map global_decl)
+    |> not syntax ? Context.proof_map (Morphism.form decl)
   end;
 
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =

--- a/src/Pure/Isar/named_target.ML	Fri Oct 28 23:10:44 2011 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 23:16:50 2011 +0200
@@ -52,12 +52,13 @@
     val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
   in
     lthy
-    |> pervasive ? Generic_Target.theory_declaration decl
+    |> pervasive ? Generic_Target.theory_declaration syntax decl
     |> Local_Theory.target (add locale locale_decl)
+    |> not syntax ? Context.proof_map (Morphism.form decl)
   end;
 
 fun target_declaration (Target {target, ...}) params =
-  if target = "" then Generic_Target.theory_declaration
+  if target = "" then Generic_Target.theory_declaration (#syntax params)
   else locale_declaration target params;
 
 

--- a/src/Pure/Isar/overloading.ML	Fri Oct 28 23:10:44 2011 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Oct 28 23:16:50 2011 +0200
@@ -206,7 +206,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = Generic_Target.theory_declaration o #syntax,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;