# HG changeset patch
# User immler
# Date 1528824762 -7200
# Node ID b0eb6a91924df43f686b131074bd00e2d84bf9bc
# Parent  38961724a017acbdba29f2eee76af157548ab2a7
tuned

diff -r 38961724a017 -r b0eb6a91924d src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:30:55 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:32:42 2018 +0200
@@ -31,10 +31,10 @@
   let
     val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
     val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
-      raise THM ("unoverload_type: no premise?", 0, [thm'])
+      raise THM ("internalize_sort': no premise?", 0, [thm'])
     val class_vars = Term.add_tvars class_premise []
     val tvar = case class_vars of [x] => TVar x | _ =>
-      raise TERM ("unoverload_type: not one type class variable.", [class_premise])
+      raise TERM ("internalize_sort': not one type class variable.", [class_premise])
   in
     (tvar, thm')
   end
@@ -45,7 +45,7 @@
     val thy = Context.theory_of context
   in
   case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
-    raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
+    raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
   | SOME (x as (_, sort)) =>
     let
       val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm