--- a/ProgTutorial/Parsing.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -625,7 +625,7 @@
 text {*
   There is usually no need to write your own parser for parsing inner syntax, that is 
   for terms and  types: you can just call the predefined parsers. Terms can 
-  be parsed using the function @{ML OuterParse.term}. For example:
+  be parsed using the function @{ML [index] term in OuterParse}. For example:
 
 @{ML_response [display,gray]
 "let 
@@ -635,10 +635,10 @@
 end"
 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
 
-  The function @{ML OuterParse.prop} is similar, except that it gives a different
+  The function @{ML [index] prop in OuterParse} is similar, except that it gives a different
   error message, when parsing fails. As you can see, the parser not just returns 
   the parsed string, but also some encoded information. You can decode the
-  information with the function @{ML YXML.parse}. For example
+  information with the function @{ML [index] parse in YXML}. For example
 
   @{ML_response [display,gray]
   "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""