--- a/ProgTutorial/Parsing.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -691,6 +691,11 @@
   in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
   \end{readmore}
   
+  FIXME:
+  @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}
+  @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}
+  
+
 *}
 
 section {* Parsing Specifications\label{sec:parsingspecs} *}