# HG changeset patch
# User wenzelm
# Date 1194732240 -3600
# Node ID 42df506673ed44e8e2d3b5c2bbedf94e4179127d
# Parent  7b9dfd4774a67446d6a8fd8bfebca87d13375377
update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);

diff -r 7b9dfd4774a6 -r 42df506673ed src/Pure/Isar/local_syntax.ML
--- 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