# HG changeset patch
# User immler
# Date 1528879523 -7200
# Node ID f9b15e7c12bd11f95898b30db559878c5082aaf2
# Parent  1b3edf5da4e4275157f4db4507fe5497969b013f
restructured

diff -r 1b3edf5da4e4 -r f9b15e7c12bd src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:38:07 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 10:45:23 2018 +0200
@@ -13,20 +13,6 @@
 structure Unoverload_Type : UNOVERLOAD_TYPE =
 struct
 
-fun those [] = []
-  | those (NONE::xs) = those xs
-  | those (SOME x::xs) = x::those xs
-
-fun params_of_sort context sort =
-  let
-    val algebra = Sign.classes_of (Context.theory_of context)
-    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
-      map (try (Axclass.get_info (Context.theory_of context))) |>
-      those |>
-      map #params |>
-      List.concat
-  in params end
-
 fun internalize_sort' ctvar thm =
   let
     val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
@@ -39,6 +25,15 @@
     (tvar, thm')
   end
 
+fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
+
+fun params_of_super_classes thy class =
+  Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
+
+fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
+
+fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty
+
 fun unoverload_single_type context x thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
@@ -49,10 +44,10 @@
   | SOME (x as (_, sort)) =>
     let
       val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
-      val consts = params_of_sort context sort |>
-        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
+      val consts = params_of_sort thy sort
+        |> map (apsnd (subst_TFree "'a" tvar) #> Const #> Thm.global_cterm_of thy)
     in
-      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
+      fold Unoverloading.unoverload consts thm'
       |> Raw_Simplifier.norm_hhf (Context.proof_of context)
     end
   end