# HG changeset patch
# User wenzelm
# Date 1379612103 -7200
# Node ID 599d8c3244772e8a52b9cd6ecbaedd62ff6805a3
# Parent  9868e6d4733f48a4abcdca27f1a18ff818288a84
repaired latex (cf. 84522727f9d3);

diff -r 9868e6d4733f -r 599d8c324477 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Thu Sep 19 18:59:28 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Thu Sep 19 19:35:03 2013 +0200
@@ -1194,7 +1194,7 @@
   \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
   "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
   a full trace of its stack of nested exceptions (if possible,
-  depending on the ML platform).}
+  depending on the ML platform).
 
   Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
   useful for debugging, but not suitable for production code.