--- a/src/Doc/IsarImplementation/ML.thy Sun Mar 02 19:00:45 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Sun Mar 02 19:45:38 2014 +0100
@@ -1159,8 +1159,8 @@
\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_exception ERROR: string} \\
+ @{index_ML_exception Fail: string} \\
@{index_ML Exn.is_interrupt: "exn -> bool"} \\
@{index_ML reraise: "exn -> 'a"} \\
@{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\