# HG changeset patch
# User wenzelm
# Date 1378905951 -7200
# Node ID addbc2387c61d3a2815f5cecc27d05fedddde1b5
# Parent  69c943125fd319b408f3048947cce88b4ca449f1
tuned message;

diff -r 69c943125fd3 -r addbc2387c61 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Sep 11 14:23:06 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Wed Sep 11 15:25:51 2013 +0200
@@ -35,14 +35,17 @@
 fun err_unresolved_overloading ctxt (c, T) t instances =
   let val ctxt' = Config.put show_variants true ctxt
   in
-    cat_lines (
-      "Unresolved overloading of constant" ::
-      quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) ::
-      "in term " ::
-      quote (Syntax.string_of_term ctxt' t) ::
-      (if null instances then "no instances" else "multiple instances:") ::
-    map (Markup.markup Markup.item o Syntax.string_of_term ctxt') instances)
-    |> error
+    error (Pretty.string_of (Pretty.chunks [
+      Pretty.block [
+        Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1,
+        Pretty.quote (Syntax.pretty_term ctxt' (Type.constraint T (Const (c, T)))),
+        Pretty.brk 1, Pretty.str "in term", Pretty.brk 1,
+        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t)]],
+      Pretty.block (
+        (if null instances then [Pretty.str "no instances"]
+        else Pretty.fbreaks (
+          Pretty.str "multiple instances:" ::
+          map (Pretty.mark Markup.item o Syntax.pretty_term ctxt') instances)))]))
   end;
 
 (* generic data *)