repaired latex (cf. 84522727f9d3);

--- 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.