--- a/ProgTutorial/FirstSteps.thy	Wed Apr 07 11:12:12 2010 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 07 11:32:00 2010 +0200
@@ -195,11 +195,18 @@
 At command \"ML\"."}
 
   This function raises the exception @{text ERROR}, which will then 
-  be displayed by the infrastructure.
+  be displayed by the infrastructure. Note that this exception is meant 
+  for ``user-level'' error messages seen by the ``end-user''.
+
+  For messages where you want to indicate a genuine program error, then
+  use the exception @{text Fail}. Here the infrastructure indicates that this 
+  is a low-level exception, and also prints the source position of the ML 
+  raise statement. 
 
 
   \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and 
   @{ML_ind profiling in Toplevel}.}
+
 *}
 
 (* FIXME*)
@@ -218,6 +225,11 @@
 *)
 
 text {*
+  %Kernel exceptions TYPE, TERM, THM also have their place in situations 
+  %where kernel-like operations are involved.  The printing is similar as for 
+  %Fail, although there is some special treatment when Toplevel.debug is 
+  %enabled.
+
   Most often you want to inspect data of Isabelle's basic data structures,
   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
   and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions