| changeset 63672 | 5a7c919a4ada |
| parent 63285 | e9c777bfd78c |
| child 63806 | c54a53ef1873 |
--- a/src/Pure/Isar/parse.ML Fri Aug 12 11:54:36 2016 +0200 +++ b/src/Pure/Isar/parse.ML Fri Aug 12 13:16:04 2016 +0200 @@ -270,7 +270,7 @@ val text = group (fn () => "text") (embedded || verbatim); -val path = group (fn () => "file name/path specification") name; +val path = group (fn () => "file name/path specification") embedded; val theory_name = group (fn () => "theory name") name;