# HG changeset patch
# User desharna
# Date 1743067113 -3600
# Node ID a3f30dc0592059a424ac600bf7bc03b537a87c69
# Parent  79a86a1ecb3d969b878d4d1f8ade8ea172e96a38
tuned

diff -r 79a86a1ecb3d -r a3f30dc05920 src/HOL/Tools/try0.ML
--- 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