src/Pure/Isar/outer_parse.ML

--- a/src/Pure/Isar/outer_parse.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -262,11 +262,11 @@
 val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)
   >> (fn (xs, T) => map (rpair T) xs);
 
-val simple_fixes = and_list1 params >> List.concat;
+val simple_fixes = and_list1 params >> flat;
 
 val fixes =
   and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
-    params >> map Syntax.no_syn) >> List.concat;
+    params >> map Syntax.no_syn) >> flat;
 
 
 (* terms *)
@@ -311,7 +311,7 @@
   ((Scan.repeat1
     (Scan.repeat1 (atom_arg is_symid blk) ||
       paren_args "(" ")" (args is_symid) ||
-      paren_args "[" "]" (args is_symid))) >> List.concat) x;
+      paren_args "[" "]" (args is_symid))) >> flat) x;
 
 val arguments = args T.is_sid false;
 
@@ -350,7 +350,7 @@
 
 val locale_fixes =
   and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) ||
-    params >> map Syntax.no_syn) >> List.concat;
+    params >> map Syntax.no_syn) >> flat;
 
 local
 
@@ -401,7 +401,7 @@
 
 val obtain_case =
   parname -- (Scan.optional (simple_fixes --| $$$ "where") [] --
-    (and_list1 (Scan.repeat1 prop) >> List.concat));
+    (and_list1 (Scan.repeat1 prop) >> flat));
 
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||