Unified treatment of type error msgs.

--- a/src/Pure/sign.ML	Fri Oct 09 14:36:48 1998 +0200
+++ b/src/Pure/sign.ML	Fri Oct 09 15:28:04 1998 +0200
@@ -602,15 +602,7 @@
         val xs = map Free bs;		(*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
-        val text = cat_lines
-         ["Type error in application: " ^ why,
-          "",
-          Pretty.string_of
-           (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
-                          Pretty.str " ::", Pretty.brk 1, prT T]),
-          Pretty.string_of
-           (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
-                          Pretty.str " ::", Pretty.brk 1, prT U]), ""];
+        val text = cat_lines(TypeInfer.appl_error prt prT why t' T u' U);
       in raise TYPE (text, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T

--- a/src/Pure/type_infer.ML	Fri Oct 09 14:36:48 1998 +0200
+++ b/src/Pure/type_infer.ML	Fri Oct 09 15:28:04 1998 +0200
@@ -11,6 +11,8 @@
     -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
     -> string list -> bool -> (indexname -> bool) -> term list -> typ list
     -> term list * typ list * (indexname * typ) list
+  val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T)
+    -> string -> term -> typ -> term -> typ -> string list
 end;
 
 structure TypeInfer: TYPE_INFER =
@@ -295,6 +297,17 @@
 
 (** type inference **)
 
+fun appl_error prt prT why t T u U =
+  ["Type error in application: " ^ why,
+   "",
+   Pretty.string_of
+    (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t,
+                   Pretty.str " ::", Pretty.brk 1, prT T]),
+   Pretty.string_of
+     (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u,
+                    Pretty.str " ::", Pretty.brk 1, prT U]),
+   ""];
+
 (* infer *)                                     (*DESTRUCTIVE*)
 
 fun infer prt prT classrel arities =
@@ -304,8 +317,6 @@
     fun unif_failed msg =
       "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
 
-    val str_of = Pretty.string_of;
-
     fun prep_output bs ts Ts =
       let
         val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
@@ -325,14 +336,8 @@
           (case T' of
             Type ("fun", _) => "Incompatible operand type."
           | _ => "Operator not of function type.");
-        val text = cat_lines
-         [unif_failed msg,
-          "Type error in application: " ^ why,
-          "",
-          str_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
-            Pretty.str " ::", Pretty.brk 1, prT T']),
-          str_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
-            Pretty.str " ::", Pretty.brk 1, prT U']), ""];
+        val text = unif_failed msg ^
+                   cat_lines (appl_error prt prT why t' T' u' U');
       in raise TYPE (text, [T', U'], [t', u']) end;
 
     fun err_constraint msg bs t T U =
@@ -340,11 +345,12 @@
         val ([t'], [T', U']) = prep_output bs [t] [T, U];
         val text = cat_lines
          [unif_failed msg,
-          "Cannot meet type constraint:",
-          "",
-          str_of (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
-            Pretty.str " ::", Pretty.brk 1, prT T']),
-          str_of (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
+          "Cannot meet type constraint:", "",
+          Pretty.string_of
+           (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
+                          Pretty.str " ::", Pretty.brk 1, prT T']),
+          Pretty.string_of
+           (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
       in raise TYPE (text, [T', U'], [t']) end;