--- 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 *)