tuned exception
authorimmler
Wed Jun 13 10:52:47 2018 +0200 (11 months ago)
changeset 68438f04d0e75e439
parent 68437 f9b15e7c12bd
child 68439 c8101022e52a
tuned exception
src/HOL/Types_To_Sets/unoverload_type.ML
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 10:45:23 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 10:52:47 2018 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4      val thy = Context.theory_of context
     1.5    in
     1.6    case find_first (fn (y, _) => x = y) tvars of NONE =>
     1.7 -    raise THM ("unoverload_type: type variable ("^(@{make_string} x)^") not in theorem", 0, [thm])
     1.8 +    raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (x,[])], [])
     1.9    | SOME (x as (_, sort)) =>
    1.10      let
    1.11        val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm