src/Pure/Isar/outer_parse.ML
changeset 8897 fb1436ca3b2e
parent 8807 0046be1769f9
child 9037 91cbae314c84
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Sun May 21 14:33:46 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun May 21 14:35:27 2000 +0200
     1.3 @@ -42,9 +42,9 @@
     1.4    val comment: token list -> Comment.text * token list
     1.5    val marg_comment: token list -> Comment.text * token list
     1.6    val interest: token list -> Comment.interest * token list
     1.7 -  val sort: token list -> xsort * token list
     1.8 -  val arity: token list -> (xsort list * xsort) * token list
     1.9 -  val simple_arity: token list -> (xsort list * xclass) * token list
    1.10 +  val sort: token list -> string * token list
    1.11 +  val arity: token list -> (string list * string) * token list
    1.12 +  val simple_arity: token list -> (string list * xclass) * token list
    1.13    val type_args: token list -> string list * token list
    1.14    val typ: token list -> string * token list
    1.15    val opt_infix: token list -> Syntax.mixfix * token list
    1.16 @@ -175,14 +175,13 @@
    1.17  
    1.18  (* sorts and arities *)
    1.19  
    1.20 -val sort =
    1.21 -  xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
    1.22 +val sort = group "sort" xname;
    1.23  
    1.24  fun gen_arity cod =
    1.25    Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
    1.26  
    1.27  val arity = gen_arity sort;
    1.28 -val simple_arity = gen_arity name;
    1.29 +val simple_arity = gen_arity xname;
    1.30  
    1.31  
    1.32  (* types *)
    1.33 @@ -266,7 +265,6 @@
    1.34    ((Scan.repeat1
    1.35      (Scan.repeat1 (atom_arg is_symid blk) ||
    1.36        paren_args "(" ")" (args is_symid) ||
    1.37 -      paren_args "{" "}" (args is_symid) ||
    1.38        paren_args "[" "]" (args is_symid))) >> flat) x;
    1.39  
    1.40