# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257554651 -3600
# Node ID 76b1b679e845772eed1e6edd16aacd3d95b130a8
# Parent  92f7328dc5ccf5df9ab5917350f4e11470e207e2
removed comment about compiler bug

diff -r 92f7328dc5cc -r 76b1b679e845 ProgTutorial/FirstSteps.thy
--- 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) *}
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\"" 
diff -r 92f7328dc5cc -r 76b1b679e845 progtutorial.pdf
Binary file progtutorial.pdf has changed