src/Pure/Thy/thy_parse.ML
changeset 8897 fb1436ca3b2e
parent 8420 f37fd19476ca
child 9328 1a46c94d1425
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Sun May 21 14:33:46 2000 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Sun May 21 14:35:27 2000 +0200
     1.3 @@ -201,13 +201,9 @@
     1.4  
     1.5  (* arities *)
     1.6  
     1.7 -val sort =
     1.8 -  name >> brackets ||
     1.9 -  "{" $$-- name_list --$$ "}";
    1.10 -
    1.11 +val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas);
    1.12  val sort_list1 = list1 sort >> mk_list;
    1.13  
    1.14 -
    1.15  val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort;
    1.16  
    1.17  val arity_decls = repeat1 (names1 --$$ "::" -- !! arity)