tuned
authorimmler
Tue Jun 12 19:32:42 2018 +0200 (11 months ago)
changeset 68430b0eb6a91924d
parent 68429 38961724a017
child 68432 6f3bd27ba389
tuned
src/HOL/Types_To_Sets/unoverload_type.ML
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:30:55 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:32:42 2018 +0200
     1.3 @@ -31,10 +31,10 @@
     1.4    let
     1.5      val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
     1.6      val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
     1.7 -      raise THM ("unoverload_type: no premise?", 0, [thm'])
     1.8 +      raise THM ("internalize_sort': no premise?", 0, [thm'])
     1.9      val class_vars = Term.add_tvars class_premise []
    1.10      val tvar = case class_vars of [x] => TVar x | _ =>
    1.11 -      raise TERM ("unoverload_type: not one type class variable.", [class_premise])
    1.12 +      raise TERM ("internalize_sort': not one type class variable.", [class_premise])
    1.13    in
    1.14      (tvar, thm')
    1.15    end
    1.16 @@ -45,7 +45,7 @@
    1.17      val thy = Context.theory_of context
    1.18    in
    1.19    case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
    1.20 -    raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
    1.21 +    raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
    1.22    | SOME (x as (_, sort)) =>
    1.23      let
    1.24        val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm