# HG changeset patch
# User immler
# Date 1528879967 -7200
# Node ID f04d0e75e439c131e5dc3fe85a54fd5d8fb21e6b
# Parent  f9b15e7c12bd11f95898b30db559878c5082aaf2
tuned exception

diff -r f9b15e7c12bd -r f04d0e75e439 src/HOL/Types_To_Sets/unoverload_type.ML
--- 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