src/Pure/sign.ML
changeset 21206 2af4c7b3f7ef
parent 21183 a76f457b6d86
child 21269 c605503bb4ef
     1.1 --- a/src/Pure/sign.ML	Tue Nov 07 11:46:47 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Nov 07 11:46:48 2006 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4    val read_term: theory -> string -> term
     1.5    val read_prop: theory -> string -> term
     1.6    val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
     1.7 -  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> theory -> theory
     1.8 +  val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.9    val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
    1.10    include SIGN_THEORY
    1.11  end
    1.12 @@ -713,8 +713,11 @@
    1.13  val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
    1.14  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
    1.15  
    1.16 -fun add_const_syntax mode args thy =
    1.17 -  thy |> add_modesyntax_i mode (map (Consts.syntax (consts_of thy)) args);
    1.18 +fun const_syntax thy (Const (c, _), mx) = SOME (Consts.syntax (consts_of thy) (c, mx))
    1.19 +  | const_syntax _ _ = NONE;
    1.20 +
    1.21 +fun add_notation mode args thy =
    1.22 +  thy |> add_modesyntax_i mode (map_filter (const_syntax thy) args);
    1.23  
    1.24  
    1.25  (* add constants *)