# HG changeset patch
# User wenzelm
# Date 952373377 -3600
# Node ID 75aaee32893da4914fe8dee3c6ae546b5ed6c893
# Parent  611342539639667f16b5fe111e8818a2e8941612
argument: include verbatim;

diff -r 611342539639 -r 75aaee32893d src/Pure/Isar/outer_parse.ML
--- 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))