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