| changeset 5930 | 41aa67a045f7 |
| parent 5922 | 85d62ecb950d |
| child 5939 | 2d7c7a4fcd8a |
--- a/src/Pure/Isar/toplevel.ML Wed Nov 18 11:03:49 1998 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Nov 18 11:12:29 1998 +0100 @@ -233,6 +233,7 @@ fun exn_message TERMINATE = "Exit." | exn_message (BREAK _) = "Break." + | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg] | exn_message Interrupt = "Interrupt (exec)." | exn_message (ERROR_MESSAGE msg) = msg | exn_message (THEORY (msg, _)) = msg