# HG changeset patch
# User wenzelm
# Date 1600954044 -7200
# Node ID 989bd067ae301a7af90bdbe91ac0b1203fb676c7
# Parent  38497ecb4892b2703689c5d68e390fae1ea92748
proper context;

diff -r 38497ecb4892 -r 989bd067ae30 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