src/Pure/Isar/outer_parse.ML

--- a/src/Pure/Isar/outer_parse.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -278,7 +278,7 @@
   ((Scan.repeat1
     (Scan.repeat1 (atom_arg is_symid blk) ||
       paren_args "(" ")" (args is_symid) ||
-      paren_args "[" "]" (args is_symid))) >> flat) x;
+      paren_args "[" "]" (args is_symid))) >> List.concat) x;
 
 val arguments = args T.is_sid false;
 
@@ -298,7 +298,7 @@
 
 val thm_sel = $$$ "(" |-- list1
   (   nat --| minus -- nat >> op upto
-   || nat >> single) --| $$$ ")" >> flat;
+   || nat >> single) --| $$$ ")" >> List.concat;
 
 val xthm = xname -- Scan.option thm_sel -- opt_attribs;
 val xthms1 = Scan.repeat1 xthm;