--- a/src/Pure/Isar/outer_parse.ML Mon Mar 06 21:08:36 2000 +0100
+++ b/src/Pure/Isar/outer_parse.ML Mon Mar 06 21:09:37 2000 +0100
@@ -250,7 +250,7 @@
(position (short_ident || long_ident || sym_ident || term_var ||
type_ident || type_var || number) >> Args.ident ||
position (keyword_symid is_symid) >> Args.keyword ||
- position string >> Args.string ||
+ position (string || verbatim) >> Args.string ||
position (if blk then $$$ "," else Scan.fail) >> Args.keyword);
fun paren_args l r scan = position ($$$ l) -- !!! (scan true -- position ($$$ r))