--- a/src/Doc/IsarImplementation/Integration.thy Sun Mar 02 19:00:45 2014 +0100
+++ b/src/Doc/IsarImplementation/Integration.thy Sun Mar 02 19:45:38 2014 +0100
@@ -48,7 +48,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type Toplevel.state} \\
- @{index_ML Toplevel.UNDEF: "exn"} \\
+ @{index_ML_exception Toplevel.UNDEF} \\
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
--- 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"} \\