proper context;
authorwenzelm
Thu, 24 Sep 2020 15:27:24 +0200
changeset 72285 989bd067ae30
parent 72284 38497ecb4892
child 72286 e4a317d00489
proper context;
src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 15:26:26 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 15:27:24 2020 +0200
@@ -157,9 +157,7 @@
       (case get_driver thy compiler of
         NONE => error ("No driver for target " ^ compiler)
       | SOME drv => drv)
-    val with_dir =
-      if Config.get (Proof_Context.init_global thy) debug
-      then with_debug_dir else Isabelle_System.with_tmp_dir
+    val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir
     fun eval result =
       with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
       |> parse_result compiler