--- a/src/HOL/Types_To_Sets/unoverload_type.ML Wed Jun 13 10:45:23 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML Wed Jun 13 10:52:47 2018 +0200
@@ -40,7 +40,7 @@
val thy = Context.theory_of context
in
case find_first (fn (y, _) => x = y) tvars of NONE =>
- raise THM ("unoverload_type: type variable ("^(@{make_string} x)^") not in theorem", 0, [thm])
+ raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (x,[])], [])
| SOME (x as (_, sort)) =>
let
val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm