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 {*