# HG changeset patch
# User wenzelm
# Date 935606358 -7200
# Node ID d98001b492b357fcb8cfb1d9a7df27c115bca22f
# Parent  1e485129fbc189170a7bb58cf5a2d0fcb71721bb
fixed arity;

diff -r 1e485129fbc1 -r d98001b492b3 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Aug 25 20:38:56 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Aug 25 20:39:18 1999 +0200
@@ -173,7 +173,7 @@
   xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
 
 fun gen_arity cod =
-  Scan.optional ($$$ "(" |-- !!! (Scan.repeat1 sort --| $$$ ")")) [] -- cod;
+  Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
 
 val arity = gen_arity sort;
 val simple_arity = gen_arity name;