# HG changeset patch
# User wenzelm
# Date 1445196601 -7200
# Node ID 1884c40f1539711706782f6f811506c55f42371a
# Parent  5b58a17c440ab9fdaf8faeaa2ed599f731d63342
tuned signature;

diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Decision_Procs/ferrante_rackoff_data.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -114,7 +114,7 @@
 || keyword npiN || keyword lin_denseN || keyword qeN 
 || keyword atomsN || keyword simpsN;
 
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
 val terms = thms >> map Drule.dest_term;
 in
 
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Decision_Procs/langford_data.ML
--- a/src/HOL/Decision_Procs/langford_data.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Decision_Procs/langford_data.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -84,7 +84,7 @@
   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   val any_keyword = keyword qeN || keyword gatherN || keyword atomsN;
 
-  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+  val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
   val terms = thms >> map Drule.dest_term;
 in
 
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun Oct 18 21:30:01 2015 +0200
@@ -41,7 +41,7 @@
     val addN = "add"
     val delN = "del"
     val any_keyword = keyword addN || keyword delN
-    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
   in
     Scan.optional (keyword addN |-- thms) [] --
      Scan.optional (keyword delN |-- thms) [] >>
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Library/Reflection.thy	Sun Oct 18 21:30:01 2015 +0200
@@ -22,7 +22,7 @@
   val onlyN = "only";
   val rulesN = "rules";
   val any_keyword = keyword onlyN || keyword rulesN;
-  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+  val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
   val terms = thms >> map (Thm.term_of o Drule.dest_term);
 in
   thms -- Scan.optional (keyword rulesN |-- thms) [] --
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -343,7 +343,7 @@
           | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
           | append_default ps = ps
 
-      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
+      in Scan.repeats sep_atom >> (rev #> append_default) end
 
     fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
       let
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 18 21:30:01 2015 +0200
@@ -400,7 +400,7 @@
     val delN = "del"
     val elimN = "elim"
     val any_keyword = keyword addN || keyword delN || simple_keyword elimN
-    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm)
   in
     Scan.optional (simple_keyword elimN >> K false) true --
     Scan.optional (keyword addN |-- thms) [] --
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -171,7 +171,7 @@
    Scan.optional (Scan.one (is_tilde o symbol) >> single) [];
 
 val long_identifier =
-  identifier @@@ (Scan.repeat1 ($$$ "." @@@ identifier) >> flat);
+  identifier @@@ Scan.repeats1 ($$$ "." @@@ identifier);
 
 val whitespace = Scan.many (is_whitespace o symbol);
 val whitespace1 = Scan.many1 (is_whitespace o symbol);
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -320,8 +320,8 @@
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x
 and parse_dependencies x =
-  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency)
-   >> (flat #> filter_out (curry (op =) "theory"))) x
+  (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency)
+   >> (filter_out (curry (op =) "theory"))) x
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    -- Scan.option ($$ "," |-- scan_general_id
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Tools/ATP/atp_satallax.ML
--- a/src/HOL/Tools/ATP/atp_satallax.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -405,7 +405,7 @@
   #>
     (if local_name <> satallaxN then
       (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-        (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
+        (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem))))
          #> fst)
     else
       (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -294,11 +294,10 @@
 
 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
 val parse_value =
-  Scan.repeat1 (Parse.minus >> single
+  Scan.repeats1 (Parse.minus >> single
                 || Scan.repeat1 (Scan.unless Parse.minus
                                              (Parse.name || Parse.float_number))
                 || @{keyword ","} |-- Parse.number >> prefix "," >> single)
-  >> flat
 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params =
   Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -897,7 +897,7 @@
 
 val constsN = "consts";
 val any_keyword = keyword constsN
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
 val terms = thms >> map (Thm.term_of o Drule.dest_term);
 
 fun optional scan = Scan.optional scan [];
diff -r 5b58a17c440a -r 1884c40f1539 src/HOL/Tools/legacy_transfer.ML
--- a/src/HOL/Tools/legacy_transfer.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -217,7 +217,7 @@
   || keyword_colon congN || keyword_colon labelsN
   || keyword_colon leavingN || keyword_colon directionN;
 
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
 val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
 
 val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -77,10 +77,10 @@
 val err_prefix = "Antiquotation lexical error: ";
 
 val scan_txt =
-  Scan.repeat1
+  Scan.repeats1
    (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) ||
     Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
-    $$$ "@" --| Scan.ahead (~$$ "{")) >> flat;
+    $$$ "@" --| Scan.ahead (~$$ "{"));
 
 val scan_antiq_body =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
@@ -101,12 +101,12 @@
 val scan_antiq =
   Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
-      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
+      (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
     (fn (pos1, (pos2, ((body, pos3), pos4))) =>
       {start = Position.set_range (pos1, pos2),
        stop = Position.set_range (pos3, pos4),
        range = Position.range pos1 pos4,
-       body = flat body});
+       body = body});
 
 val scan_antiquote =
   scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/General/scan.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -57,6 +57,8 @@
   val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+  val repeats: ('a -> 'b list * 'a) -> 'a -> 'b list * 'a
+  val repeats1: ('a -> 'b list * 'a) -> 'a -> 'b list * 'a
   val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
@@ -191,6 +193,9 @@
 
 fun repeat1 scan = scan ::: repeat scan;
 
+fun repeats scan = repeat scan >> flat;
+fun repeats1 scan = repeat1 scan >> flat;
+
 fun single scan = scan >> (fn x => [x]);
 fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
 
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/General/symbol_pos.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -118,11 +118,10 @@
 fun scan_strs q err_prefix =
   Scan.ahead ($$ q) |--
     !!! (fn () => err_prefix ^ "unclosed string literal")
-      ((scan_pos --| $$$ q) --
-        ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
+      ((scan_pos --| $$$ q) -- (Scan.repeats (scan_str q err_prefix) -- ($$$ q |-- scan_pos)));
 
 fun recover_strs q =
-  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
+  $$$ q @@@ Scan.repeats (Scan.permissive (scan_str q ""));
 
 in
 
@@ -202,7 +201,7 @@
   Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
   Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
 
-val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
+val scan_cmts = Scan.pass 0 (Scan.repeats scan_cmt);
 
 in
 
@@ -266,7 +265,7 @@
 
 in
 
-val scan_ident = letter ::: (Scan.repeat (letdigs1 || sub ::: letdigs1) >> flat);
+val scan_ident = letter ::: Scan.repeats (letdigs1 || sub ::: letdigs1);
 
 end;
 
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -281,7 +281,7 @@
 
 val thm = gen_thm Facts.the_single;
 val multi_thm = gen_thm (K I);
-val thms = Scan.repeat multi_thm >> flat;
+val thms = Scan.repeats multi_thm;
 
 end;
 
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/method.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -526,7 +526,7 @@
 local
 
 fun thms ss =
-  Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
+  Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm);
 
 fun app {init, attribute, pos = _} ths context =
   fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context);
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -421,10 +421,7 @@
 
     fun args blk x = Scan.optional (args1 blk) [] x
     and args1 blk x =
-      ((Scan.repeat1
-        (Scan.repeat1 (argument blk) ||
-          argsp "(" ")" ||
-          argsp "[" "]")) >> flat) x
+      (Scan.repeats1 (Scan.repeat1 (argument blk) || argsp "(" ")" || argsp "[" "]")) x
     and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x;
   in (args, args1) end;
 
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/token.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -551,10 +551,10 @@
   Scan.ahead ($$ "{" -- $$ "*") |--
     !!! "unclosed verbatim text"
       ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
-        ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
+        (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
 
 val recover_verbatim =
-  $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
+  $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb;
 
 
 (* scan cartouche *)
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -198,7 +198,7 @@
 val scan_ident = scan_alphanumeric || scan_symbolic;
 
 val scan_long_ident =
-  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
+  Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "=");
 
 val scan_type_var = $$$ "'" @@@ scan_letdigs;
 
@@ -249,7 +249,7 @@
   $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
 
 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
-val scan_gaps = Scan.repeat scan_gap >> flat;
+val scan_gaps = Scan.repeats scan_gap;
 
 in
 
@@ -262,10 +262,10 @@
 val scan_string =
   Scan.ahead ($$ "\"") |--
     !!! "unclosed string literal"
-      ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
+      ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\"");
 
 val recover_string =
-  $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
+  $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str);
 
 end;
 
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/PIDE/xml.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -239,12 +239,12 @@
 
 fun parse_content xs =
   (parse_optional_text @@@
-    (Scan.repeat
+    Scan.repeats
       ((parse_element >> single ||
         parse_cdata >> (single o Text) ||
         parse_processing_instruction ||
         parse_comment)
-      @@@ parse_optional_text) >> flat)) xs
+      @@@ parse_optional_text)) xs
 
 and parse_element xs =
   ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -94,7 +94,7 @@
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 val scan_id = Symbol_Pos.scan_ident;
-val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
+val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id);
 val scan_tid = $$$ "'" @@@ scan_id;
 
 val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
@@ -238,12 +238,12 @@
 val scan_str =
   Scan.ahead ($$ "'" -- $$ "'") |--
     !!! "unclosed string literal"
-      ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
+      ($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'");
 
 val scan_str_body =
   Scan.ahead ($$ "'" |-- $$ "'") |--
     !!! "unclosed string literal"
-      ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
+      ($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'");
 
 fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss));
 val explode_str = explode_literal scan_str_body;
diff -r 5b58a17c440a -r 1884c40f1539 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Tools/rail.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -104,7 +104,7 @@
     [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
 
 val scan =
-  (Scan.repeat scan_token >> flat) --|
+  Scan.repeats scan_token --|
     Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
       (Scan.ahead (Scan.one Symbol_Pos.is_eof));