| changeset 54387 | 890e983cb07b |
| parent 53709 | 84522727f9d3 |
| child 54389 | a4051679a7bf |
--- a/src/Pure/ML/ml_compiler_polyml.ML Mon Nov 11 18:37:56 2013 +0100 +++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Nov 11 20:00:53 2013 +0100 @@ -36,6 +36,8 @@ val exn_messages_ids = Runtime.exn_messages_ids exn_info; val exn_messages = Runtime.exn_messages exn_info; val exn_message = Runtime.exn_message exn_info; + +val exn_error_message = Output.error_message o exn_message; fun exn_trace e = print_exception_trace exn_message e;