src/HOL/Library/code_test.ML
changeset 69623 ef02c5e051e5
parent 69597 ff784d5a5bfb
child 69626 0631421c6d6a
--- a/src/HOL/Library/code_test.ML	Mon Jan 07 18:50:41 2019 +0100
+++ b/src/HOL/Library/code_test.ML	Thu Jan 10 12:07:05 2019 +0000
@@ -164,7 +164,9 @@
       | SOME f => f)
     val debug = Config.get (Proof_Context.init_global thy) overlord
     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
-    fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
+    fun evaluate result =
+      with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
+      |> parse_result compiler
     fun evaluator program _ vs_ty deps =
       Exn.interruptible_capture evaluate
         (Code_Target.compilation_text ctxt target program deps true vs_ty)