diff -r c80aba8c1d5e -r fb1436ca3b2e src/Pure/Isar/outer_parse.ML
--- 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;