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 =>