# HG changeset patch
# User wenzelm
# Date 1662634990 -7200
# Node ID 8d6cb72aa5110a25dbadf005710956546db2fe81
# Parent  1202e29798a4babc64d72654800ed08bf8104e50
tuned output: more Pretty.item;

diff -r 1202e29798a4 -r 8d6cb72aa511 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Thu Sep 08 12:52:41 2022 +0200
+++ b/src/Pure/goal_display.ML	Thu Sep 08 13:03:10 2022 +0200
@@ -72,7 +72,7 @@
       Syntax.unparse_term ctxt;
 
     fun prt_atoms prt prtT (X, xs) = Pretty.block
-      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
+      [Pretty.item (Pretty.commas (map prt xs)), Pretty.str " ::",
         Pretty.brk 1, prtT X];
 
     fun prt_var (x, ~1) = prt_term (Syntax.free x)
@@ -93,7 +93,7 @@
       Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
     val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
 
-    val pretty_ffpairs = pretty_list "flex-flex pairs:" (Pretty.block o Syntax.pretty_flexpair ctxt);
+    val pretty_ffpairs = pretty_list "flex-flex pairs:" (Pretty.item o Syntax.pretty_flexpair ctxt);
 
     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
     val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
diff -r 1202e29798a4 -r 8d6cb72aa511 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Sep 08 12:52:41 2022 +0200
+++ b/src/Pure/proofterm.ML	Thu Sep 08 13:03:10 2022 +0200
@@ -1860,7 +1860,7 @@
         fun search _ [] =
               error ("Unsolvable constraints:\n" ^
                 Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
-                  Pretty.block (Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
+                  Pretty.item (Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
                     (apply2 (Envir.norm_term bigenv) p))) cs)))
           | search env ((u, p as (t1, t2), vs)::ps) =
               if u then