diff -r 28a49fe024c9 -r 304426a9aecf ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue Nov 03 13:57:03 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Thu Nov 05 10:30:59 2009 +0100
@@ -694,7 +694,8 @@
   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}
-  
+  @{ML_ind read_term in Syntax} @{ML_ind read_term in Syntax}
+
 
 *}