--- a/src/Pure/thm.ML Sun Feb 09 12:58:40 2025 +0100
+++ b/src/Pure/thm.ML Sun Feb 09 13:11:20 2025 +0100
@@ -1886,10 +1886,9 @@
Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ_global thy ty];
val msg =
- Pretty.string_of (Pretty.block
- [Pretty.str "instantiate: type conflict",
- Pretty.fbrk, pretty_typing (Var v) T,
- Pretty.fbrk, pretty_typing u U])
+ Pretty.string_of (Pretty.big_list "instantiate: type conflict"
+ [Pretty.item [pretty_typing (Var v) T],
+ Pretty.item [pretty_typing u U]]);
in raise TYPE (msg, [T, U], [Var v, u]) end;
fun prep_insts (instT, inst) (cert, sorts) =