# HG changeset patch
# User desharna
# Date 1696000939 -7200
# Node ID a0f85118488cbfcd5a833ac512dbbcbaf4435be1
# Parent  046e2ddff9ba2fd9a2d54a0fef54ba9d3f6d9654
moved variable bindings to tighter scope

diff -r 046e2ddff9ba -r a0f85118488c src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Sep 29 15:52:56 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Sep 29 17:22:19 2023 +0200
@@ -160,14 +160,15 @@
 fun run_sledgehammer (params as {provers, ...}) output_dir keep_probs keep_proofs
     exhaustive_preplay thy_index trivial pos st =
   let
-    val thy = Proof.theory_of st
-    val thy_long_name = Context.theory_long_name thy
-    val session_name = Long_Name.qualifier thy_long_name
-    val thy_name = Long_Name.base_name thy_long_name
     val triv_str = if trivial then "[T] " else ""
     val keep =
       if keep_probs orelse keep_proofs then
-        let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
+        let
+          val thy_long_name = Context.theory_long_name (Proof.theory_of st)
+          val session_name = Long_Name.qualifier thy_long_name
+          val thy_name = Long_Name.base_name thy_long_name
+          val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name
+        in
           Path.append (Path.append output_dir (Path.basic session_name)) (Path.basic subdir)
           |> Isabelle_System.make_directory
           |> Path.implode