src/HOL/Types_To_Sets/unoverload_type.ML
changeset 68429 38961724a017
parent 68428 46beee72fb66
child 68430 b0eb6a91924d
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 16:21:52 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:30:55 2018 +0200
     1.3 @@ -27,6 +27,18 @@
     1.4        List.concat
     1.5    in params end
     1.6  
     1.7 +fun internalize_sort' ctvar thm =
     1.8 +  let
     1.9 +    val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
    1.10 +    val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
    1.11 +      raise THM ("unoverload_type: no premise?", 0, [thm'])
    1.12 +    val class_vars = Term.add_tvars class_premise []
    1.13 +    val tvar = case class_vars of [x] => TVar x | _ =>
    1.14 +      raise TERM ("unoverload_type: not one type class variable.", [class_premise])
    1.15 +  in
    1.16 +    (tvar, thm')
    1.17 +  end
    1.18 +
    1.19  fun unoverload_type context s thm =
    1.20    let
    1.21      val tvars = Term.add_tvars (Thm.prop_of thm) []
    1.22 @@ -36,7 +48,7 @@
    1.23      raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
    1.24    | SOME (x as (_, sort)) =>
    1.25      let
    1.26 -      val (tvar, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
    1.27 +      val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
    1.28        val consts = params_of_sort context sort |>
    1.29          map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
    1.30      in