# HG changeset patch
# User wenzelm
# Date 1194732236 -3600
# Node ID 2e766dd19e4f66ef2777e36e1d2d06f25a98a672
# Parent  72cfe89f7b218d731cd3603b6e008ed71decc9d5
notation: based on Syntax.update_const_gram (avoids duplicates);

diff -r 72cfe89f7b21 -r 2e766dd19e4f src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Nov 10 23:03:52 2007 +0100
+++ b/src/Pure/sign.ML	Sat Nov 10 23:03:56 2007 +0100
@@ -644,11 +644,12 @@
 val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
 
-fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
-  | const_syntax _ _ = NONE;
-
-fun notation add mode args thy = thy
-  |> (if add then add_modesyntax_i else del_modesyntax_i) mode (map_filter (const_syntax thy) args);
+fun notation add mode args thy =
+  let
+    val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
+    fun const_syntax (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
+      | const_syntax _ = NONE;
+  in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
 
 
 (* add constants *)