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