src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
changeset 73374 316e12147698
parent 72518 4be6ae020fc4
child 73428 9d1b5c0bdec8
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Mar 04 10:10:44 2021 +0100
@@ -158,7 +158,6 @@
         Path.explode dest_dir + problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir)
-    val exec = exec full_proofs
     val command0 =
       (case find_first (fn var => getenv var <> "") (fst exec) of
         SOME var =>