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