notation: based on Syntax.update_const_gram (avoids duplicates);
authorwenzelm
Sat Nov 10 23:03:56 2007 +0100 (2007-11-10)
changeset 253832e766dd19e4f
parent 25382 72cfe89f7b21
child 25384 7b9dfd4774a6
notation: based on Syntax.update_const_gram (avoids duplicates);
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sat Nov 10 23:03:52 2007 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Nov 10 23:03:56 2007 +0100
     1.3 @@ -644,11 +644,12 @@
     1.4  val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
     1.5  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
     1.6  
     1.7 -fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
     1.8 -  | const_syntax _ _ = NONE;
     1.9 -
    1.10 -fun notation add mode args thy = thy
    1.11 -  |> (if add then add_modesyntax_i else del_modesyntax_i) mode (map_filter (const_syntax thy) args);
    1.12 +fun notation add mode args thy =
    1.13 +  let
    1.14 +    val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
    1.15 +    fun const_syntax (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
    1.16 +      | const_syntax _ = NONE;
    1.17 +  in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
    1.18  
    1.19  
    1.20  (* add constants *)