--- a/src/HOL/Tools/Argo/argo_tactic.ML Sun Oct 31 23:41:07 2021 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Mon Nov 01 11:52:24 2021 +0100
@@ -221,7 +221,7 @@
fun trace_props props ctxt =
tracing ctxt (Pretty.string_of (Pretty.big_list "using these propositions:"
- (map (Syntax.pretty_term ctxt) props)))
+ (map (Pretty.item o single o Syntax.pretty_term ctxt) props)))
fun trace_result ctxt ({elapsed, ...}: Timing.timing) msg =
tracing ctxt ("found a " ^ msg ^ " in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")