# HG changeset patch
# User wenzelm
# Date 1635763944 -3600
# Node ID d1117655110cb05bd47ddd99189e24121afe4c69
# Parent  b31683a544cf147311943d15dd54c7ef1df3d29d
tuned message;

diff -r b31683a544cf -r d1117655110c src/HOL/Tools/Argo/argo_tactic.ML
--- 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")