src/HOL/Tools/Mirabelle/mirabelle_try0.ML
changeset 81362 f586fdabe670
parent 76183 8089593a364a
child 81363 fec95447c5bd
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Tue Oct 22 14:34:13 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Tue Oct 22 17:31:54 2024 +0200
@@ -14,7 +14,7 @@
     val generous_timeout = Time.scale 10.0 timeout
 
     fun run ({pre, ...} : Mirabelle.command) =
-      if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then
+      if Timeout.apply generous_timeout (not o null o Try0.try0 (SOME timeout) ([], [], [], [])) pre then
         "succeeded"
       else
         ""