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