src/HOL/Tools/Mirabelle/mirabelle_try0.ML
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
         ""