# HG changeset patch
# User wenzelm
# Date 1287255731 -3600
# Node ID 84e1f8d8f30ab63a45cfda8e2e93ca1b160aae6b
# Parent  d4299b4158794cb80b94d7b465f66272c14c146f
tuned;

diff -r d4299b415879 -r 84e1f8d8f30a doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sat Oct 16 11:34:46 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sat Oct 16 20:02:11 2010 +0100
@@ -376,7 +376,7 @@
   \paragraph{Program failures.}  There is a handful of standard
   exceptions that indicate general failure situations, or failures of
   core operations on logical entities (types, terms, theorems,
-  theories).
+  theories, see \chref{ch:logic}).
 
   These exceptions indicate a genuine breakdown of the program, so the
   main purpose is to determine quickly what has happened where.
@@ -428,8 +428,10 @@
   \begin{mldecls}
   @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
   @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
+  @{index_ML ERROR: "string -> exn"} \\
+  @{index_ML Fail: "string -> exn"} \\
+  @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML reraise: "exn -> 'a"} \\
-  @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
@@ -444,14 +446,20 @@
 
   \item @{ML can} is similar to @{ML try} with more abstract result.
 
+  \item @{ML ERROR}~@{text "msg"} represents user errors; this
+  exception is always raised via the @{ML error} function (see
+  \secref{sec:message-channels}).
+
+  \item @{ML Fail}~@{text "msg"} represents general program failures.
+
+  \item @{ML Exn.is_interrupt} identifies interrupts robustly, without
+  mentioning concrete exception constructors in user code.  Handled
+  interrupts need to be re-raised promptly!
+
   \item @{ML reraise}~@{text "exn"} raises exception @{text "exn"}
   while preserving its implicit position information (if possible,
   depending on the ML platform).
 
-  \item @{ML Exn.is_interrupt} identifies interrupts robustly, without
-  having to mention concrete exception constructors in user code.
-  Handled interrupts need to be re-raised promptly!
-
   \item @{ML exception_trace}~@{verbatim "(fn _ =>"}~@{text
   "e"}@{verbatim ")"} evaluates expression @{text "e"} while printing
   a full trace of its stack of nested exceptions (if possible,