src/Pure/Isar/parse.ML

--- a/src/Pure/Isar/parse.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -65,7 +65,7 @@
   val binding: binding parser
   val xname: xstring parser
   val text: string parser
-  val path: Path.T parser
+  val path: string parser
   val liberal_name: xstring parser
   val parname: string parser
   val parbinding: binding parser
@@ -250,7 +250,7 @@
 val text = group (fn () => "text")
   (short_ident || long_ident || sym_ident || string || number || verbatim);
 
-val path = group (fn () => "file name/path specification") name >> Path.explode;
+val path = group (fn () => "file name/path specification") name;
 
 val liberal_name = keyword_ident_or_symbolic || xname;