# HG changeset patch
# User desharna
# Date 1740743185 -3600
# Node ID 9807c44f5d5755158a6714ec9c156ba62d5e80aa
# Parent  b3502f81ab3d7071918668e60d4647d7c54fab2a
tuned: restricted visibility of definitions

diff -r b3502f81ab3d -r 9807c44f5d57 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Feb 28 11:36:59 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Feb 28 12:46:25 2025 +0100
@@ -66,6 +66,8 @@
 
 type result = {name: string, command: string, time: Time.time, state: Proof.state}
 
+local
+
 fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt tagged st :
   result option =
   if mode <> Auto_Try orelse run_if_auto_try then
@@ -115,7 +117,7 @@
 val no_attrs = []
 
 (* name * ((all_goals, run_if_auto_try), tags *)
-val named_methods =
+val raw_named_methods =
   [("simp", ((false, true), simp_attrs)),
    ("auto", ((true, true), full_attrs)),
    ("blast", ((false, true), clas_attrs)),
@@ -131,7 +133,12 @@
    ("satx", ((false, false), no_attrs)),
    ("order", ((false, true), no_attrs))]
 
-val apply_methods = map apply_named_method named_methods
+in
+
+val named_methods = map fst raw_named_methods
+val apply_methods = map apply_named_method raw_named_methods
+
+end
 
 fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
 fun tool_time_string (s, time) = s ^ ": " ^ time_string time
@@ -166,7 +173,7 @@
         |> the_list
   in
     if mode = Normal then
-      "Trying " ^ implode_space (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
+      "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^
       "..."
       |> writeln
     else