# HG changeset patch
# User wenzelm
# Date 1725278237 -7200
# Node ID 3f740fa101f7b31a67d2971f5e07baa73d5604f2
# Parent  f0c754a98e52e3aa1e22f8a13ea796d6cedfe996
tuned: prefer Symbol.spaces;

diff -r f0c754a98e52 -r 3f740fa101f7 src/HOL/Tools/SMT/z3_proof.ML
--- a/src/HOL/Tools/SMT/z3_proof.ML	Mon Sep 02 13:42:38 2024 +0200
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Mon Sep 02 13:57:17 2024 +0200
@@ -121,7 +121,7 @@
 fun string_of_node ctxt =
   let
     fun str depth (Z3_Node {id, rule, prems, concl, bounds}) =
-      replicate_string depth "  " ^
+      Symbol.spaces (2 * depth) ^
       enclose "{" "}" (commas
         [string_of_int id,
          string_of_rule rule,
diff -r f0c754a98e52 -r 3f740fa101f7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Sep 02 13:42:38 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Sep 02 13:57:17 2024 +0200
@@ -384,7 +384,7 @@
 
     fun add_str s' = apfst (suffix s')
 
-    fun of_indent ind = replicate_string (ind * indent_size) " "
+    fun of_indent ind = Symbol.spaces (ind * indent_size)
     fun of_moreover ind = of_indent ind ^ "moreover\n"
     fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
 
@@ -443,7 +443,7 @@
         val prefix = "{ "
         val suffix = " }"
       in
-        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+        Symbol.spaces (ind * indent_size - size prefix) ^ prefix ^
         String.substring (s, ind * indent_size, size s - ind * indent_size - 1) ^
         suffix ^ "\n"
       end
diff -r f0c754a98e52 -r 3f740fa101f7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Sep 02 13:42:38 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Sep 02 13:57:17 2024 +0200
@@ -160,10 +160,10 @@
         let
           val (l0, r0) = chop (length xs div 2) xs
 (*
-          val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
-          val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs))
-          val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0))
-          val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0))
+          val _ = warning (Symbol.spaces depth ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
+          val _ = warning (Symbol.spaces depth ^ " " ^ "xs: " ^ n_facts (map fst xs))
+          val _ = warning (Symbol.spaces depth ^ " " ^ "l0: " ^ n_facts (map fst l0))
+          val _ = warning (Symbol.spaces depth ^ " " ^ "r0: " ^ n_facts (map fst r0))
 *)
           val depth = depth + 1
           val timeout = new_timeout timeout run_time
@@ -186,7 +186,7 @@
               in (sup, (l @ r, result)) end))
         end
 (*
-        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
+        |> tap (fn _ => warning (Symbol.spaces depth ^ "}"))
 *)
       | min _ result sup xs = (sup, (xs, result))
   in
diff -r f0c754a98e52 -r 3f740fa101f7 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Mon Sep 02 13:42:38 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Mon Sep 02 13:57:17 2024 +0200
@@ -41,7 +41,7 @@
 fun print_isar_skeleton ctxt indent keyword stmt =
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
-    val prefix = replicate_string indent " ";
+    val prefix = Symbol.spaces indent;
     val prefix_sep = "\n" ^ prefix ^ "    and ";
     val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
     val if_s = if null assms then NONE
@@ -59,7 +59,7 @@
 fun print_skeleton ctxt indent keyword stmt =
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
-    val prefix = replicate_string indent " ";
+    val prefix = Symbol.spaces indent;
     val prefix_sep = "\n" ^ prefix ^ "  and ";
     val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
     val assumes_s = if null assms then NONE
@@ -87,7 +87,7 @@
 fun print_subgoal apply_line_opt (is_prems, is_for, is_sh) ctxt indent stmt =
   let
     val ((fixes, _, _), ctxt') = eigen_context_for_statement stmt ctxt;
-    val prefix = replicate_string indent " ";
+    val prefix = Symbol.spaces indent;
     val fixes_s =
       if not is_for orelse null fixes then NONE
       else SOME ("for " ^ space_implode " "