changeset 56265 | 785569927666 |
parent 55837 | 154855d9a564 |
child 56275 | 600f432ab556 |
--- a/src/Pure/ML/ml_compiler_polyml.ML Sun Mar 23 16:40:35 2014 +0100 +++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Mar 24 12:00:17 2014 +0100 @@ -78,6 +78,7 @@ let val _ = Secure.secure_mltext (); val space = ML_Env.name_space; + val opt_context = Context.thread_data (); (* input *) @@ -168,7 +169,7 @@ | SOME code => apply_result ((code - |> Runtime.debugging exn_message + |> Runtime.debugging exn_message opt_context |> Runtime.toplevel_error (err o exn_message)) ())));