--- 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;
--- 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