# HG changeset patch
# User wenzelm
# Date 1739103080 -3600
# Node ID c30b6eff8fa1ae04b8948170e77e144c9ef88de3
# Parent  f67fb2339eeb9dcb06b6b73912a37fbc7c320547
tuned message;

diff -r f67fb2339eeb -r c30b6eff8fa1 src/Pure/thm.ML
--- 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) =