--- a/ProgTutorial/FirstSteps.thy	Sat Nov 07 01:03:37 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sat Nov 07 01:44:11 2009 +0100
@@ -202,7 +202,8 @@
   @{ML_ind profiling in Toplevel}.}
 *}
 
-(* FIXME
+(* FIXME*)
+(*
 ML {* reset Toplevel.debug *}
 
 ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}

--- a/ProgTutorial/Parsing.thy	Sat Nov 07 01:03:37 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Sat Nov 07 01:44:11 2009 +0100
@@ -412,9 +412,7 @@
   @{ML_ind scan in OuterSyntax}. It is given the argument 
   @{ML "Position.none"} since,
   at the moment, we are not interested in generating precise error
-  messages. The following code\footnote{Note that because of a possible bug in
-  the PolyML runtime system, the result is printed as @{text [quotes] "?"},
-  instead of the tokens.}
+  messages. The following code
 
 
 @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" 

Binary file progtutorial.pdf has changed