uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);

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

--- a/src/Pure/Isar/generic_target.ML	Sat Oct 29 12:55:34 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat Oct 29 12:57:43 2011 +0200
@@ -193,7 +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)
+    |> 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/local_theory.ML	Sat Oct 29 12:55:34 2011 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Oct 29 12:57:43 2011 +0200
@@ -231,8 +231,7 @@
 fun alias global_alias local_alias b name =
   declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b
-    in Context.mapping (global_alias b' name) (local_alias b' name) end)
-  #> local_alias b name;
+    in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
 val class_alias = alias Sign.class_alias Proof_Context.class_alias;
 val type_alias = alias Sign.type_alias Proof_Context.type_alias;

--- a/src/Pure/Isar/named_target.ML	Sat Oct 29 12:55:34 2011 +0200
+++ b/src/Pure/Isar/named_target.ML	Sat Oct 29 12:57:43 2011 +0200
@@ -54,7 +54,6 @@
     lthy
     |> 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 =