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) *}