--- a/src/Pure/Isar/outer_parse.ML Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML Sun May 21 14:35:27 2000 +0200
@@ -42,9 +42,9 @@
val comment: token list -> Comment.text * token list
val marg_comment: token list -> Comment.text * token list
val interest: token list -> Comment.interest * token list
- val sort: token list -> xsort * token list
- val arity: token list -> (xsort list * xsort) * token list
- val simple_arity: token list -> (xsort list * xclass) * token list
+ val sort: token list -> string * token list
+ val arity: token list -> (string list * string) * token list
+ val simple_arity: token list -> (string list * xclass) * token list
val type_args: token list -> string list * token list
val typ: token list -> string * token list
val opt_infix: token list -> Syntax.mixfix * token list
@@ -175,14 +175,13 @@
(* sorts and arities *)
-val sort =
- xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
+val sort = group "sort" xname;
fun gen_arity cod =
Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
val arity = gen_arity sort;
-val simple_arity = gen_arity name;
+val simple_arity = gen_arity xname;
(* types *)
@@ -266,7 +265,6 @@
((Scan.repeat1
(Scan.repeat1 (atom_arg is_symid blk) ||
paren_args "(" ")" (args is_symid) ||
- paren_args "{" "}" (args is_symid) ||
paren_args "[" "]" (args is_symid))) >> flat) x;