1.1 --- a/NEWS	Sat Oct 29 12:55:34 2011 +0200
     1.2 +++ b/NEWS	Sat Oct 29 12:57:43 2011 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  ProofContext has been discontinued.  INCOMPATIBILITY.
     1.5  
     1.6  * Refined Local_Theory.declaration {syntax, pervasive}, with subtle
     1.7 -change of semantics for syntax = false: update is applied to auxiliary
     1.8 +change of semantics: update is applied to auxiliary local theory
     1.9  context as well.
    1.10  
    1.11  

     2.1 --- a/src/Pure/Isar/generic_target.ML	Sat Oct 29 12:55:34 2011 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Sat Oct 29 12:57:43 2011 +0200
     2.3 @@ -193,7 +193,7 @@
     2.4      lthy
     2.5      |> Local_Theory.background_theory (Context.theory_map global_decl)
     2.6      |> Local_Theory.target (Context.proof_map global_decl)
     2.7 -    |> not syntax ? Context.proof_map (Morphism.form decl)
     2.8 +    |> Context.proof_map (Morphism.form decl)
     2.9    end;
    2.10  
    2.11  fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =

     3.1 --- a/src/Pure/Isar/local_theory.ML	Sat Oct 29 12:55:34 2011 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Oct 29 12:57:43 2011 +0200
     3.3 @@ -231,8 +231,7 @@
     3.4  fun alias global_alias local_alias b name =
     3.5    declaration {syntax = true, pervasive = false} (fn phi =>
     3.6      let val b' = Morphism.binding phi b
     3.7 -    in Context.mapping (global_alias b' name) (local_alias b' name) end)
     3.8 -  #> local_alias b name;
     3.9 +    in Context.mapping (global_alias b' name) (local_alias b' name) end);
    3.10  
    3.11  val class_alias = alias Sign.class_alias Proof_Context.class_alias;
    3.12  val type_alias = alias Sign.type_alias Proof_Context.type_alias;

     4.1 --- a/src/Pure/Isar/named_target.ML	Sat Oct 29 12:55:34 2011 +0200
     4.2 +++ b/src/Pure/Isar/named_target.ML	Sat Oct 29 12:57:43 2011 +0200
     4.3 @@ -54,7 +54,6 @@
     4.4      lthy
     4.5      |> pervasive ? Generic_Target.theory_declaration syntax decl
     4.6      |> Local_Theory.target (add locale locale_decl)
     4.7 -    |> not syntax ? Context.proof_map (Morphism.form decl)
     4.8    end;
     4.9  
    4.10  fun target_declaration (Target {target, ...}) params =