--- a/src/HOL/Tools/try0.ML Thu Mar 27 10:06:43 2025 +0100
+++ b/src/HOL/Tools/try0.ML Thu Mar 27 10:18:33 2025 +0100
@@ -219,24 +219,24 @@
val metis_attrs = [(Simp, ""), (Intro, ""), (Elim, ""), (Dest, "")]
val no_attrs = []
-(* name * ((all_goals, run_if_auto_try), tags *)
+(* name * (run_if_auto_try * (all_goals * tags)) *)
val raw_named_methods =
- [("simp", ((false, true), simp_attrs)),
- ("auto", ((true, true), full_attrs)),
- ("blast", ((false, true), clas_attrs)),
- ("metis", ((false, true), metis_attrs)),
- ("argo", ((false, true), no_attrs)),
- ("linarith", ((false, true), no_attrs)),
- ("presburger", ((false, true), no_attrs)),
- ("algebra", ((false, true), no_attrs)),
- ("fast", ((false, false), clas_attrs)),
- ("fastforce", ((false, false), full_attrs)),
- ("force", ((false, false), full_attrs)),
- ("meson", ((false, false), metis_attrs)),
- ("satx", ((false, false), no_attrs)),
- ("order", ((false, true), no_attrs))]
+ [("simp", (true, (false, simp_attrs))),
+ ("auto", (true, (true, full_attrs))),
+ ("blast", (true, (false, clas_attrs))),
+ ("metis", (true, (false, metis_attrs))),
+ ("argo", (true, (false, no_attrs))),
+ ("linarith", (true, (false, no_attrs))),
+ ("presburger", (true, (false, no_attrs))),
+ ("algebra", (true, (false, no_attrs))),
+ ("fast", (false, (false, clas_attrs))),
+ ("fastforce", (false, (false, full_attrs))),
+ ("force", (false, (false, full_attrs))),
+ ("meson", (false, (false, metis_attrs))),
+ ("satx", (false, (false, no_attrs))),
+ ("order", (true, (false, no_attrs)))]
-fun apply_raw_named_method (name, ((all_goals, _), attrs)) timeout_opt tagged st :
+fun apply_raw_named_method name (all_goals, attrs) timeout_opt tagged st :
result option =
let
val unused =
@@ -276,16 +276,14 @@
else NONE
end
-fun apply_proof_method name timeout_opt (tagged : tagged_xref list) st : result option =
- (case AList.lookup (op =) raw_named_methods name of
- NONE => NONE
- | SOME raw_method => apply_raw_named_method (name, raw_method) timeout_opt tagged st)
-
in
-val () = List.app (fn (name, ((_, run_if_auto_try), _)) =>
- register_proof_method name {run_if_auto_try = run_if_auto_try} (apply_proof_method name)
- handle Symtab.DUP _ => ()) raw_named_methods
+val () = raw_named_methods
+ |> List.app (fn (name, (run_if_auto_try, raw_method)) =>
+ let val meth : proof_method = apply_raw_named_method name raw_method in
+ register_proof_method name {run_if_auto_try = run_if_auto_try} meth
+ handle Symtab.DUP _ => ()
+ end)
end