tuned exceptions -- avoid composing error messages in low-level situations;

--- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 12 14:54:14 2013 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 12 15:30:38 2013 +0200
@@ -107,9 +107,8 @@
     val insts' = map (apfst mapT_and_recertify) insts;
   in Thm.instantiate (instTs, insts') end;
 
-fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
-  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
-  [TVar (ixn, S), TVar (ixn, S')], []);
+fun tvar_clash ixn S S' =
+  raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []);
 
 fun lookup (tye, (ixn, S)) =
   (case AList.lookup (op =) tye ixn of

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Apr 12 14:54:14 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Apr 12 15:30:38 2013 +0200
@@ -478,7 +478,7 @@
 
 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
    one of the premises. Unfortunately, this sometimes yields "Variable
-   ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
+   has two distinct types" errors. To avoid this, we instantiate the
    variables before applying "assume_tac". Typical constraints are of the form
      ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
    where the nonvariables are goal parameters. *)

--- a/src/Pure/envir.ML	Fri Apr 12 14:54:14 2013 +0200
+++ b/src/Pure/envir.ML	Fri Apr 12 15:30:38 2013 +0200
@@ -106,8 +106,7 @@
   in (env', v) end;
 
 fun var_clash xi T T' =
-  raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types",
-    [T', T], []);
+  raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]);
 
 fun lookup_check check tenv (xi, T) =
   (case Vartab.lookup tenv xi of

--- a/src/Pure/type.ML	Fri Apr 12 14:54:14 2013 +0200
+++ b/src/Pure/type.ML	Fri Apr 12 15:30:38 2013 +0200
@@ -416,9 +416,8 @@
 
 type tyenv = (sort * typ) Vartab.table;
 
-fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
-  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
-  [TVar (ixn, S), TVar (ixn, S')], []);
+fun tvar_clash ixn S S' =
+  raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []);
 
 fun lookup tye (ixn, S) =
   (case Vartab.lookup tye ixn of