--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 10 12:44:49 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 10 14:04:52 2024 +0200
@@ -94,7 +94,7 @@
val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms)
val concl = Syntax.pretty_term ctxt concl
in
- tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
+ tracing (Pretty.string_of (Pretty.block (Pretty.breaks [time, assms, concl])))
end
fun take_time timeout tac arg =