diff -r 92f7328dc5cc -r 76b1b679e845 ProgTutorial/Parsing.thy
--- 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\""