src/Pure/sign.ML
changeset 56240 938c6c7e10eb
parent 56239 17df7145a871
child 59841 2551ac44150e
     1.1 --- a/src/Pure/sign.ML	Fri Mar 21 10:45:03 2014 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Mar 21 11:06:39 2014 +0100
     1.3 @@ -73,12 +73,10 @@
     1.4    val add_nonterminals: Proof.context -> binding list -> theory -> theory
     1.5    val add_nonterminals_global: binding list -> theory -> theory
     1.6    val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
     1.7 -  val add_syntax: (string * typ * mixfix) list -> theory -> theory
     1.8 -  val add_syntax_cmd: (string * string * mixfix) list -> theory -> theory
     1.9 -  val add_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    1.10 -  val add_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.11 -  val del_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    1.12 -  val del_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.13 +  val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    1.14 +  val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.15 +  val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    1.16 +  val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.17    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
    1.18    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.19    val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
    1.20 @@ -375,12 +373,10 @@
    1.21  
    1.22  fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
    1.23  
    1.24 -val add_modesyntax = gen_add_syntax (K I);
    1.25 -val add_modesyntax_cmd = gen_add_syntax Syntax.read_typ;
    1.26 -val add_syntax = add_modesyntax Syntax.mode_default;
    1.27 -val add_syntax_cmd = add_modesyntax_cmd Syntax.mode_default;
    1.28 -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) (K I);
    1.29 -val del_modesyntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
    1.30 +val add_syntax = gen_add_syntax (K I);
    1.31 +val add_syntax_cmd = gen_add_syntax Syntax.read_typ;
    1.32 +val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I);
    1.33 +val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
    1.34  
    1.35  fun type_notation add mode args =
    1.36    let
    1.37 @@ -417,7 +413,7 @@
    1.38    in
    1.39      thy
    1.40      |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
    1.41 -    |> add_syntax (map #2 args)
    1.42 +    |> add_syntax Syntax.mode_default (map #2 args)
    1.43      |> pair (map #3 args)
    1.44    end;
    1.45