--- a/src/Pure/Isar/outer_parse.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML Fri Dec 15 00:08:06 2006 +0100
@@ -220,7 +220,7 @@
val name = group "name declaration" (short_ident || sym_ident || string || number);
val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
-val path = group "file name/path specification" name >> Path.unpack;
+val path = group "file name/path specification" name >> Path.explode;
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";