--- a/src/Pure/Isar/parse.ML Tue May 24 16:03:03 2016 +0200
+++ b/src/Pure/Isar/parse.ML Tue May 24 16:13:59 2016 +0200
@@ -268,9 +268,7 @@
(cartouche || string || short_ident || long_ident || sym_ident ||
term_var || type_ident || type_var || number);
-val text =
- group (fn () => "text")
- (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche);
+val text = group (fn () => "text") (embedded || verbatim);
val path = group (fn () => "file name/path specification") name;