# HG changeset patch
# User wenzelm
# Date 1738753873 -3600
# Node ID 2b4892e30a42ec4f3c7f5518ed025c89450e24fc
# Parent  d72a4ecf8c2030d353b0cf346cf522375ea2c41f
misc tuning;

diff -r d72a4ecf8c20 -r 2b4892e30a42 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 05 12:00:14 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 05 12:11:13 2025 +0100
@@ -162,11 +162,11 @@
           opts @ options ctxt
   in solver_info_of (K []) all_options ctxt end;
 
-val setup_solver =
-  Attrib.setup \<^binding>\<open>smt_solver\<close>
+val _ =
+  Theory.setup (Attrib.setup \<^binding>\<open>smt_solver\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
-    "SMT solver configuration";
+    "SMT solver configuration");
 
 
 (* options *)
@@ -237,23 +237,17 @@
     let val dir = Resources.master_directory (Context.theory_of context) + Path.explode name
     in SOME (Cache_IO.unsynchronized_init dir) end);
 
-val setup_certificates =
-  Attrib.setup \<^binding>\<open>smt_certificates\<close>
+val _ =
+  Theory.setup (Attrib.setup \<^binding>\<open>smt_certificates\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
-    "SMT certificates configuration";
+    "SMT certificates configuration");
 
 
-(* setup *)
-
-val _ = Theory.setup (
-  setup_solver #>
-  setup_certificates);
+(* print_setup *)
 
 fun print_setup ctxt =
   let
-    fun string_of_bool b = if b then "true" else "false";
-
     val names = available_solvers_of ctxt;
     val ns = if null names then ["(none)"] else sort_strings names;
     val n = the_default "(none)" (get_solver ctxt);
@@ -271,11 +265,9 @@
       Pretty.str ("Current SMT solver options: " ^ implode_space opts),
       Pretty.str_list "Available SMT solvers: "  "" ns,
       Pretty.str ("Current timeout: " ^ t ^ " seconds"),
-      Pretty.str ("With proofs: " ^
-        string_of_bool (not (Config.get ctxt oracle))),
+      Pretty.str ("With proofs: " ^ Value.print_bool (not (Config.get ctxt oracle))),
       Pretty.str ("Certificates cache: " ^ certs_filename),
-      Pretty.str ("Fixed certificates: " ^
-        string_of_bool (Config.get ctxt read_only_certificates))])
+      Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))])
   end;
 
 val _ =