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

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

     3.1 --- a/src/Pure/Isar/generic_target.ML	Fri Oct 28 23:10:44 2011 +0200
     3.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Oct 28 23:16:50 2011 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4      string * bool -> (binding * mixfix) * term -> local_theory ->
     3.5      (term * term) * local_theory
     3.6  
     3.7 -  val theory_declaration: declaration -> local_theory -> local_theory
     3.8 +  val theory_declaration: bool -> declaration -> local_theory -> local_theory
     3.9    val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    3.10      term list * term list -> local_theory -> (term * thm) * local_theory
    3.11    val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
    3.12 @@ -185,7 +185,7 @@
    3.13  
    3.14  (** primitive theory operations **)
    3.15  
    3.16 -fun theory_declaration decl lthy =
    3.17 +fun theory_declaration syntax decl lthy =
    3.18    let
    3.19      val global_decl = Morphism.form
    3.20        (Morphism.transform (Local_Theory.global_morphism lthy) decl);
    3.21 @@ -193,6 +193,7 @@
    3.22      lthy
    3.23      |> Local_Theory.background_theory (Context.theory_map global_decl)
    3.24      |> Local_Theory.target (Context.proof_map global_decl)
    3.25 +    |> not syntax ? Context.proof_map (Morphism.form decl)
    3.26    end;
    3.27  
    3.28  fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =

     4.1 --- a/src/Pure/Isar/named_target.ML	Fri Oct 28 23:10:44 2011 +0200
     4.2 +++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 23:16:50 2011 +0200
     4.3 @@ -52,12 +52,13 @@
     4.4      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
     4.5    in
     4.6      lthy
     4.7 -    |> pervasive ? Generic_Target.theory_declaration decl
     4.8 +    |> pervasive ? Generic_Target.theory_declaration syntax decl
     4.9      |> Local_Theory.target (add locale locale_decl)
    4.10 +    |> not syntax ? Context.proof_map (Morphism.form decl)
    4.11    end;
    4.12  
    4.13  fun target_declaration (Target {target, ...}) params =
    4.14 -  if target = "" then Generic_Target.theory_declaration
    4.15 +  if target = "" then Generic_Target.theory_declaration (#syntax params)
    4.16    else locale_declaration target params;
    4.17  
    4.18  

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