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