common Type.appl_error, which also covers explicit constraints;

--- a/src/Pure/sign.ML	Sun Sep 12 19:04:02 2010 +0200
+++ b/src/Pure/sign.ML	Sun Sep 12 19:55:45 2010 +0200
@@ -265,12 +265,12 @@
 
 fun type_check pp tm =
   let
-    fun err_appl why bs t T u U =
+    fun err_appl bs t T u U =
       let
         val xs = map Free bs;           (*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
-        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
+        val msg = Type.appl_error pp t' T u' U;
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
@@ -283,8 +283,8 @@
           let val T = typ_of (bs, t) and U = typ_of (bs, u) in
             (case T of
               Type ("fun", [T1, T2]) =>
-                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
-            | _ => err_appl "Operator not of function type" bs t T u U)
+                if T1 = U then T2 else err_appl bs t T u U
+            | _ => err_appl bs t T u U)
           end;
   in typ_of ([], tm) end;
 

--- a/src/Pure/type.ML	Sun Sep 12 19:04:02 2010 +0200
+++ b/src/Pure/type.ML	Sun Sep 12 19:55:45 2010 +0200
@@ -9,6 +9,7 @@
 sig
   (*constraints*)
   val constraint: typ -> term -> term
+  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
   datatype decl =
     LogicalType of int |
@@ -104,6 +105,28 @@
   if T = dummyT then t
   else Const ("_type_constraint_", T --> T) $ t;
 
+fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
+      cat_lines
+       ["Failed to meet type constraint:", "",
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
+          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
+  | appl_error pp t T u U =
+      cat_lines
+       ["Type error in application: " ^
+          (case T of
+            Type ("fun", _) => "incompatible operand type"
+          | _ => "operator not of function type"),
+        "",
+        Pretty.string_of (Pretty.block
+          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
+            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
+        Pretty.string_of (Pretty.block
+          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
+            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
+
 
 
 (** type signatures and certified types **)

--- a/src/Pure/type_infer.ML	Sun Sep 12 19:04:02 2010 +0200
+++ b/src/Pure/type_infer.ML	Sun Sep 12 19:55:45 2010 +0200
@@ -13,7 +13,6 @@
   val paramify_vars: typ -> typ
   val paramify_dummies: typ -> int -> typ * int
   val fixate_params: Name.context -> term list -> term list
-  val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
   val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
     term list -> term list
@@ -318,29 +317,12 @@
 
 (** type inference **)
 
-(* appl_error *)
-
-fun appl_error pp why t T u U =
- ["Type error in application: " ^ why,
-  "",
-  Pretty.string_of (Pretty.block
-    [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
-      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
-  Pretty.string_of (Pretty.block
-    [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
-      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
-  ""];
-
-
 (* infer *)
 
 fun infer pp tsig =
   let
     (* errors *)
 
-    fun unif_failed msg =
-      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
-
     fun prep_output tye bs ts Ts =
       let
         val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
@@ -353,27 +335,21 @@
     fun err_loose i =
       raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
 
+    fun unif_failed msg =
+      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
+
     fun err_appl msg tye bs t T u U =
       let
         val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
-        val why =
-          (case T' of
-            Type ("fun", _) => "Incompatible operand type"
-          | _ => "Operator not of function type");
-        val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
+        val text = unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n";
       in raise TYPE (text, [T', U'], [t', u']) end;
 
     fun err_constraint msg tye bs t T U =
       let
         val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
-        val text = cat_lines
-         [unif_failed msg,
-          "Cannot meet type constraint:", "",
-          Pretty.string_of (Pretty.block
-           [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
-            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
-          Pretty.string_of (Pretty.block
-           [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
+        val text =
+          unif_failed msg ^
+            Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n";
       in raise TYPE (text, [T', U'], [t']) end;