ProgTutorial/Parsing.thy
changeset 473 fea1b7ce5c4a
parent 472 1bbe4268664d
child 514 7e25716c3744
--- 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: