--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 09 11:51:52 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 09 12:06:08 2024 +0100
@@ -278,8 +278,11 @@
val indent_size = 2
fun pretty_maybe_quote ctxt pretty =
- let val s = Pretty.unformatted_string_of pretty
- in if ATP_Util.maybe_quote ctxt s = s then pretty else Pretty.quote pretty end
+ let val s = Pretty.unformatted_string_of pretty in
+ if ATP_Util.maybe_quote ctxt s = s then pretty
+ else if Config.get ctxt ATP_Util.proof_cartouches then Pretty.cartouche pretty
+ else Pretty.quote pretty
+ end
val hashw = ATP_Util.hashw
val hashw_string = ATP_Util.hashw_string