diff -r 1bbe4268664d -r fea1b7ce5c4a ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sun Jul 31 00:00:58 2011 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Oct 17 13:30:49 2011 +0100
@@ -783,7 +783,7 @@
 
   \begin{readmore}
   The functions to do with input and output of XML and YXML are defined 
-  in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
+  in @{ML_file "Pure/PIDE/xml.ML"} and @{ML_file "Pure/PIDE/yxml.ML"}.
   \end{readmore}
   
   FIXME: