--- a/src/Pure/more_thm.ML Thu Sep 08 12:43:40 2022 +0200
+++ b/src/Pure/more_thm.ML Thu Sep 08 12:52:41 2022 +0200
@@ -731,7 +731,7 @@
if hlen = 0 then []
else if show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
+ (map (q o Pretty.block o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
map (Syntax.pretty_sort ctxt) extra_shyps)]
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
val tsymbs =