diff -r 154855d9a564 -r e120a15b0ee6 src/Doc/IsarImplementation/ML.thy
--- 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"} \\