diff -r 05e6a33edef6 -r 14173c0e8688 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Aug 04 16:18:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 05 08:58:28 2009 +0200
@@ -165,6 +165,10 @@
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
+  This function raises the exception @{text ERROR} which will then 
+  be displayed by the infrastructure.
+
+
   (FIXME Mention how to work with @{ML [index] debug in Toplevel} and 
   @{ML [index] profiling in Toplevel}.)
 *}
@@ -2257,7 +2261,7 @@
 
 ML {*Datatype.get_info @{theory} "List.list"*}
 
-section {* Name Space(TBD) *}
+section {* Name Space Issues (TBD) *}
 
 
 end