1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Sun Oct 18 20:48:24 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Sun Oct 18 21:30:01 2015 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4  || keyword npiN || keyword lin_denseN || keyword qeN 
     1.5  || keyword atomsN || keyword simpsN;
     1.6  
     1.7 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
     1.8 +val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
     1.9  val terms = thms >> map Drule.dest_term;
    1.10  in
    1.11  

     2.1 --- a/src/HOL/Decision_Procs/langford_data.ML	Sun Oct 18 20:48:24 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/langford_data.ML	Sun Oct 18 21:30:01 2015 +0200
     2.3 @@ -84,7 +84,7 @@
     2.4    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
     2.5    val any_keyword = keyword qeN || keyword gatherN || keyword atomsN;
     2.6  
     2.7 -  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
     2.8 +  val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
     2.9    val terms = thms >> map Drule.dest_term;
    2.10  in
    2.11  

     3.1 --- a/src/HOL/Groebner_Basis.thy	Sun Oct 18 20:48:24 2015 +0200
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Oct 18 21:30:01 2015 +0200
     3.3 @@ -41,7 +41,7 @@
     3.4      val addN = "add"
     3.5      val delN = "del"
     3.6      val any_keyword = keyword addN || keyword delN
     3.7 -    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
     3.8 +    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
     3.9    in
    3.10      Scan.optional (keyword addN |-- thms) [] --
    3.11       Scan.optional (keyword delN |-- thms) [] >>

     4.1 --- a/src/HOL/Library/Reflection.thy	Sun Oct 18 20:48:24 2015 +0200
     4.2 +++ b/src/HOL/Library/Reflection.thy	Sun Oct 18 21:30:01 2015 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    val onlyN = "only";
     4.5    val rulesN = "rules";
     4.6    val any_keyword = keyword onlyN || keyword rulesN;
     4.7 -  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
     4.8 +  val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
     4.9    val terms = thms >> map (Thm.term_of o Drule.dest_term);
    4.10  in
    4.11    thms -- Scan.optional (keyword rulesN |-- thms) [] --

     5.1 --- a/src/HOL/Library/rewrite.ML	Sun Oct 18 20:48:24 2015 +0200
     5.2 +++ b/src/HOL/Library/rewrite.ML	Sun Oct 18 21:30:01 2015 +0200
     5.3 @@ -343,7 +343,7 @@
     5.4            | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
     5.5            | append_default ps = ps
     5.6  
     5.7 -      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
     5.8 +      in Scan.repeats sep_atom >> (rev #> append_default) end
     5.9  
    5.10      fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
    5.11        let

     6.1 --- a/src/HOL/Presburger.thy	Sun Oct 18 20:48:24 2015 +0200
     6.2 +++ b/src/HOL/Presburger.thy	Sun Oct 18 21:30:01 2015 +0200
     6.3 @@ -400,7 +400,7 @@
     6.4      val delN = "del"
     6.5      val elimN = "elim"
     6.6      val any_keyword = keyword addN || keyword delN || simple_keyword elimN
     6.7 -    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
     6.8 +    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm)
     6.9    in
    6.10      Scan.optional (simple_keyword elimN >> K false) true --
    6.11      Scan.optional (keyword addN |-- thms) [] --

     7.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Oct 18 20:48:24 2015 +0200
     7.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Oct 18 21:30:01 2015 +0200
     7.3 @@ -171,7 +171,7 @@
     7.4     Scan.optional (Scan.one (is_tilde o symbol) >> single) [];
     7.5  
     7.6  val long_identifier =
     7.7 -  identifier @@@ (Scan.repeat1 ($$$ "." @@@ identifier) >> flat);
     7.8 +  identifier @@@ Scan.repeats1 ($$$ "." @@@ identifier);
     7.9  
    7.10  val whitespace = Scan.many (is_whitespace o symbol);
    7.11  val whitespace1 = Scan.many1 (is_whitespace o symbol);

     8.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Oct 18 20:48:24 2015 +0200
     8.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Oct 18 21:30:01 2015 +0200
     8.3 @@ -320,8 +320,8 @@
     8.4    (parse_inference_source >> snd
     8.5     || scan_general_id --| skip_term >> single) x
     8.6  and parse_dependencies x =
     8.7 -  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency)
     8.8 -   >> (flat #> filter_out (curry (op =) "theory"))) x
     8.9 +  (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency)
    8.10 +   >> (filter_out (curry (op =) "theory"))) x
    8.11  and parse_file_source x =
    8.12    (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    8.13     -- Scan.option ($$ "," |-- scan_general_id

     9.1 --- a/src/HOL/Tools/ATP/atp_satallax.ML	Sun Oct 18 20:48:24 2015 +0200
     9.2 +++ b/src/HOL/Tools/ATP/atp_satallax.ML	Sun Oct 18 21:30:01 2015 +0200
     9.3 @@ -405,7 +405,7 @@
     9.4    #>
     9.5      (if local_name <> satallaxN then
     9.6        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
     9.7 -        (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
     9.8 +        (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem))))
     9.9           #> fst)
    9.10      else
    9.11        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())

    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Sun Oct 18 20:48:24 2015 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Sun Oct 18 21:30:01 2015 +0200
    10.3 @@ -294,11 +294,10 @@
    10.4  
    10.5  val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
    10.6  val parse_value =
    10.7 -  Scan.repeat1 (Parse.minus >> single
    10.8 +  Scan.repeats1 (Parse.minus >> single
    10.9                  || Scan.repeat1 (Scan.unless Parse.minus
   10.10                                               (Parse.name || Parse.float_number))
   10.11                  || @{keyword ","} |-- Parse.number >> prefix "," >> single)
   10.12 -  >> flat
   10.13  val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
   10.14  val parse_params =
   10.15    Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []

    11.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 18 20:48:24 2015 +0200
    11.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 18 21:30:01 2015 +0200
    11.3 @@ -897,7 +897,7 @@
    11.4  
    11.5  val constsN = "consts";
    11.6  val any_keyword = keyword constsN
    11.7 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    11.8 +val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
    11.9  val terms = thms >> map (Thm.term_of o Drule.dest_term);
   11.10  
   11.11  fun optional scan = Scan.optional scan [];

    12.1 --- a/src/HOL/Tools/legacy_transfer.ML	Sun Oct 18 20:48:24 2015 +0200
    12.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Sun Oct 18 21:30:01 2015 +0200
    12.3 @@ -217,7 +217,7 @@
    12.4    || keyword_colon congN || keyword_colon labelsN
    12.5    || keyword_colon leavingN || keyword_colon directionN;
    12.6  
    12.7 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    12.8 +val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
    12.9  val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
   12.10  
   12.11  val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)

    13.1 --- a/src/Pure/General/antiquote.ML	Sun Oct 18 20:48:24 2015 +0200
    13.2 +++ b/src/Pure/General/antiquote.ML	Sun Oct 18 21:30:01 2015 +0200
    13.3 @@ -77,10 +77,10 @@
    13.4  val err_prefix = "Antiquotation lexical error: ";
    13.5  
    13.6  val scan_txt =
    13.7 -  Scan.repeat1
    13.8 +  Scan.repeats1
    13.9     (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) ||
   13.10      Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
   13.11 -    $$$ "@" --| Scan.ahead (~$$ "{")) >> flat;
   13.12 +    $$$ "@" --| Scan.ahead (~$$ "{"));
   13.13  
   13.14  val scan_antiq_body =
   13.15    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   13.16 @@ -101,12 +101,12 @@
   13.17  val scan_antiq =
   13.18    Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
   13.19      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
   13.20 -      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
   13.21 +      (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
   13.22      (fn (pos1, (pos2, ((body, pos3), pos4))) =>
   13.23        {start = Position.set_range (pos1, pos2),
   13.24         stop = Position.set_range (pos3, pos4),
   13.25         range = Position.range pos1 pos4,
   13.26 -       body = flat body});
   13.27 +       body = body});
   13.28  
   13.29  val scan_antiquote =
   13.30    scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;

    14.1 --- a/src/Pure/General/scan.ML	Sun Oct 18 20:48:24 2015 +0200
    14.2 +++ b/src/Pure/General/scan.ML	Sun Oct 18 21:30:01 2015 +0200
    14.3 @@ -57,6 +57,8 @@
    14.4    val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    14.5    val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    14.6    val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    14.7 +  val repeats: ('a -> 'b list * 'a) -> 'a -> 'b list * 'a
    14.8 +  val repeats1: ('a -> 'b list * 'a) -> 'a -> 'b list * 'a
    14.9    val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   14.10    val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   14.11    val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
   14.12 @@ -191,6 +193,9 @@
   14.13  
   14.14  fun repeat1 scan = scan ::: repeat scan;
   14.15  
   14.16 +fun repeats scan = repeat scan >> flat;
   14.17 +fun repeats1 scan = repeat1 scan >> flat;
   14.18 +
   14.19  fun single scan = scan >> (fn x => [x]);
   14.20  fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
   14.21  

    15.1 --- a/src/Pure/General/symbol_pos.ML	Sun Oct 18 20:48:24 2015 +0200
    15.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Oct 18 21:30:01 2015 +0200
    15.3 @@ -118,11 +118,10 @@
    15.4  fun scan_strs q err_prefix =
    15.5    Scan.ahead ($$ q) |--
    15.6      !!! (fn () => err_prefix ^ "unclosed string literal")
    15.7 -      ((scan_pos --| $$$ q) --
    15.8 -        ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
    15.9 +      ((scan_pos --| $$$ q) -- (Scan.repeats (scan_str q err_prefix) -- ($$$ q |-- scan_pos)));
   15.10  
   15.11  fun recover_strs q =
   15.12 -  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
   15.13 +  $$$ q @@@ Scan.repeats (Scan.permissive (scan_str q ""));
   15.14  
   15.15  in
   15.16  
   15.17 @@ -202,7 +201,7 @@
   15.18    Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
   15.19    Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
   15.20  
   15.21 -val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
   15.22 +val scan_cmts = Scan.pass 0 (Scan.repeats scan_cmt);
   15.23  
   15.24  in
   15.25  
   15.26 @@ -266,7 +265,7 @@
   15.27  
   15.28  in
   15.29  
   15.30 -val scan_ident = letter ::: (Scan.repeat (letdigs1 || sub ::: letdigs1) >> flat);
   15.31 +val scan_ident = letter ::: Scan.repeats (letdigs1 || sub ::: letdigs1);
   15.32  
   15.33  end;
   15.34  

    16.1 --- a/src/Pure/Isar/attrib.ML	Sun Oct 18 20:48:24 2015 +0200
    16.2 +++ b/src/Pure/Isar/attrib.ML	Sun Oct 18 21:30:01 2015 +0200
    16.3 @@ -281,7 +281,7 @@
    16.4  
    16.5  val thm = gen_thm Facts.the_single;
    16.6  val multi_thm = gen_thm (K I);
    16.7 -val thms = Scan.repeat multi_thm >> flat;
    16.8 +val thms = Scan.repeats multi_thm;
    16.9  
   16.10  end;
   16.11  

    17.1 --- a/src/Pure/Isar/method.ML	Sun Oct 18 20:48:24 2015 +0200
    17.2 +++ b/src/Pure/Isar/method.ML	Sun Oct 18 21:30:01 2015 +0200
    17.3 @@ -526,7 +526,7 @@
    17.4  local
    17.5  
    17.6  fun thms ss =
    17.7 -  Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
    17.8 +  Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm);
    17.9  
   17.10  fun app {init, attribute, pos = _} ths context =
   17.11    fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context);

    18.1 --- a/src/Pure/Isar/parse.ML	Sun Oct 18 20:48:24 2015 +0200
    18.2 +++ b/src/Pure/Isar/parse.ML	Sun Oct 18 21:30:01 2015 +0200
    18.3 @@ -421,10 +421,7 @@
    18.4  
    18.5      fun args blk x = Scan.optional (args1 blk) [] x
    18.6      and args1 blk x =
    18.7 -      ((Scan.repeat1
    18.8 -        (Scan.repeat1 (argument blk) ||
    18.9 -          argsp "(" ")" ||
   18.10 -          argsp "[" "]")) >> flat) x
   18.11 +      (Scan.repeats1 (Scan.repeat1 (argument blk) || argsp "(" ")" || argsp "[" "]")) x
   18.12      and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x;
   18.13    in (args, args1) end;
   18.14  

    19.1 --- a/src/Pure/Isar/token.ML	Sun Oct 18 20:48:24 2015 +0200
    19.2 +++ b/src/Pure/Isar/token.ML	Sun Oct 18 21:30:01 2015 +0200
    19.3 @@ -551,10 +551,10 @@
    19.4    Scan.ahead ($$ "{" -- $$ "*") |--
    19.5      !!! "unclosed verbatim text"
    19.6        ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
    19.7 -        ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
    19.8 +        (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
    19.9  
   19.10  val recover_verbatim =
   19.11 -  $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
   19.12 +  $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb;
   19.13  
   19.14  
   19.15  (* scan cartouche *)

    20.1 --- a/src/Pure/ML/ml_lex.ML	Sun Oct 18 20:48:24 2015 +0200
    20.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Oct 18 21:30:01 2015 +0200
    20.3 @@ -198,7 +198,7 @@
    20.4  val scan_ident = scan_alphanumeric || scan_symbolic;
    20.5  
    20.6  val scan_long_ident =
    20.7 -  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
    20.8 +  Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "=");
    20.9  
   20.10  val scan_type_var = $$$ "'" @@@ scan_letdigs;
   20.11  
   20.12 @@ -249,7 +249,7 @@
   20.13    $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
   20.14  
   20.15  val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
   20.16 -val scan_gaps = Scan.repeat scan_gap >> flat;
   20.17 +val scan_gaps = Scan.repeats scan_gap;
   20.18  
   20.19  in
   20.20  
   20.21 @@ -262,10 +262,10 @@
   20.22  val scan_string =
   20.23    Scan.ahead ($$ "\"") |--
   20.24      !!! "unclosed string literal"
   20.25 -      ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
   20.26 +      ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\"");
   20.27  
   20.28  val recover_string =
   20.29 -  $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
   20.30 +  $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str);
   20.31  
   20.32  end;
   20.33  

    21.1 --- a/src/Pure/PIDE/xml.ML	Sun Oct 18 20:48:24 2015 +0200
    21.2 +++ b/src/Pure/PIDE/xml.ML	Sun Oct 18 21:30:01 2015 +0200
    21.3 @@ -239,12 +239,12 @@
    21.4  
    21.5  fun parse_content xs =
    21.6    (parse_optional_text @@@
    21.7 -    (Scan.repeat
    21.8 +    Scan.repeats
    21.9        ((parse_element >> single ||
   21.10          parse_cdata >> (single o Text) ||
   21.11          parse_processing_instruction ||
   21.12          parse_comment)
   21.13 -      @@@ parse_optional_text) >> flat)) xs
   21.14 +      @@@ parse_optional_text)) xs
   21.15  
   21.16  and parse_element xs =
   21.17    ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--

    22.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Oct 18 20:48:24 2015 +0200
    22.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Oct 18 21:30:01 2015 +0200
    22.3 @@ -94,7 +94,7 @@
    22.4  fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
    22.5  
    22.6  val scan_id = Symbol_Pos.scan_ident;
    22.7 -val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
    22.8 +val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id);
    22.9  val scan_tid = $$$ "'" @@@ scan_id;
   22.10  
   22.11  val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
   22.12 @@ -238,12 +238,12 @@
   22.13  val scan_str =
   22.14    Scan.ahead ($$ "'" -- $$ "'") |--
   22.15      !!! "unclosed string literal"
   22.16 -      ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
   22.17 +      ($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'");
   22.18  
   22.19  val scan_str_body =
   22.20    Scan.ahead ($$ "'" |-- $$ "'") |--
   22.21      !!! "unclosed string literal"
   22.22 -      ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
   22.23 +      ($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'");
   22.24  
   22.25  fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss));
   22.26  val explode_str = explode_literal scan_str_body;

    23.1 --- a/src/Pure/Tools/rail.ML	Sun Oct 18 20:48:24 2015 +0200
    23.2 +++ b/src/Pure/Tools/rail.ML	Sun Oct 18 21:30:01 2015 +0200
    23.3 @@ -104,7 +104,7 @@
    23.4      [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
    23.5  
    23.6  val scan =
    23.7 -  (Scan.repeat scan_token >> flat) --|
    23.8 +  Scan.repeats scan_token --|
    23.9      Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
   23.10        (Scan.ahead (Scan.one Symbol_Pos.is_eof));
   23.11