diff -r 7fee9141da5e -r 7816e7be7bc7 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Mar 28 08:24:07 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Mar 28 08:56:13 2025 +0100
@@ -173,8 +173,7 @@
 fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt
 
 fun try0_trans (facts : facts) =
-  Toplevel.keep_proof
-    (ignore o generic_try0 Normal (SOME default_timeout) facts o Toplevel.proof_of)
+  Toplevel.keep_proof (ignore o try0 (SOME default_timeout) facts o Toplevel.proof_of)
 
 val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)