# HG changeset patch # User wenzelm # Date 1365773438 -7200 # Node ID 1e29891759c444d264f638a086f48edb7c686c24 # Parent c8f2bad67dbbe5e0887fea050ca6090d7b825376 tuned exceptions -- avoid composing error messages in low-level situations; diff -r c8f2bad67dbb -r 1e29891759c4 src/HOL/Statespace/distinct_tree_prover.ML --- 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 diff -r c8f2bad67dbb -r 1e29891759c4 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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. *) diff -r c8f2bad67dbb -r 1e29891759c4 src/Pure/envir.ML --- 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 diff -r c8f2bad67dbb -r 1e29891759c4 src/Pure/type.ML --- 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