update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);

--- a/src/Pure/Isar/local_syntax.ML	Sat Nov 10 23:03:57 2007 +0100
+++ b/src/Pure/Isar/local_syntax.ML	Sat Nov 10 23:04:00 2007 +0100
@@ -59,7 +59,7 @@
   let
     val thy_syntax = Sign.syn_of thy;
     val is_logtype = Sign.is_logtype thy;
-    fun const_gram ((true, m), decls) = Syntax.extend_const_gram is_logtype m decls
+    fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
       | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
     val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
     val local_syntax = thy_syntax