src/Pure/ML/ml_compiler_polyml.ML
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)) ())));