# HG changeset patch
# User wenzelm
# Date 1393785938 -3600
# Node ID e120a15b0ee6a3993d5fe2d4c4c026fbbd10d6c9
# Parent  154855d9a56483b7ba8d869087c1665044a73e92
more antiquotations;

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