
diff -r fe45fbb111c5 -r abc7f90188af ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Fri Apr 03 07:55:07 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Apr 07 17:04:39 2009 +0100
@@ -748,6 +748,11 @@
   \end{exercise}
 *}
 
+text {*
+  (FIXME: @{ML OuterParse.type_args}, @{ML OuterParse.typ}, @{ML OuterParse.opt_mixfix})
+*}
+
+
 section {* New Commands and Keyword Files\label{sec:newcommand} *}
 
 text {*




