src/HOL/Library/code_test.ML
changeset 72376 04bce3478688
parent 72375 e48d93811ed7
child 72511 460d743010bc
--- a/src/HOL/Library/code_test.ML	Mon Oct 05 21:15:58 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Mon Oct 05 22:07:25 2020 +0200
@@ -140,11 +140,10 @@
 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
 
 fun with_debug_dir name f =
-  let
-    val dir =
-      Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
-    val _ = Isabelle_System.make_directory dir
-  in Exn.release (Exn.capture f dir) end
+  Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+  |> Isabelle_System.make_directory
+  |> Exn.capture f
+  |> Exn.release;
 
 fun dynamic_value_strict ctxt t compiler =
   let