# HG changeset patch
# User immler
# Date 1547855547 18000
# Node ID 33843320448f243712faeeb13cc4f4de6e4233cd
# Parent  b18353d3fe1ab12e22c1ed9660a76a14460c6987
restore type variable names in unoverload_type

diff -r b18353d3fe1a -r 33843320448f src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Fri Jan 18 21:36:13 2019 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Fri Jan 18 18:52:27 2019 -0500
@@ -804,7 +804,7 @@
 interpretation local_typedef_module_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
 
 lemmas_with [var_simplified explicit_ab_group_add,
-  unoverload_type 'e 'b,
+    unoverload_type 'e 'f,
   OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_module_pair_on_with,
   untransferred,
   var_simplified implicit_ab_group_add]:
@@ -849,7 +849,7 @@
 interpretation local_typedef_vector_space_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
 
 lemmas_with [var_simplified explicit_ab_group_add,
-    unoverload_type 'e 'b,
+    unoverload_type 'e 'f,
   OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_vector_space_pair_on_with,
   folded lt1.dim_S_def lt2.dim_S_def,
   untransferred,
@@ -967,7 +967,7 @@
 interpretation local_typedef_finite_dimensional_vector_space_pair_1 S1 scale1 Basis1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
 
 lemmas_with [var_simplified explicit_ab_group_add,
-    unoverload_type 'e 'b,
+    unoverload_type 'e 'f,
   OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_1_on_with,
   folded lt1.dim_S_def lt2.dim_S_def,
   untransferred,
@@ -999,7 +999,7 @@
 interpretation local_typedef_finite_dimensional_vector_space_pair S1 scale1 Basis1 "TYPE('s)" S2 scale2 Basis2 "TYPE('t)" by unfold_locales fact+
 
 lemmas_with [var_simplified explicit_ab_group_add,
-    unoverload_type 'e 'b,
+    unoverload_type 'e 'f,
   OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_on_with,
   folded lt1.dim_S_def lt2.dim_S_def,
   untransferred,
diff -r b18353d3fe1a -r 33843320448f src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Fri Jan 18 21:36:13 2019 +0100
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Fri Jan 18 18:52:27 2019 -0500
@@ -13,18 +13,6 @@
 structure Unoverload_Type : UNOVERLOAD_TYPE =
 struct
 
-fun internalize_sort' ctvar thm =
-  let
-    val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
-    val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
-      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 ("internalize_sort': not one type class variable.", [class_premise])
-  in
-    (tvar, thm')
-  end
-
 fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
 
 fun params_of_super_classes thy class =
@@ -34,20 +22,31 @@
 
 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 =
+fun unoverload_single_type context tvar thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
     val thy = Context.theory_of context
   in
-  case find_first (fn (y, _) => x = y) tvars of NONE =>
-    raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (x,[])], [])
+  case find_first (fn (y, _) => tvar = y) tvars of NONE =>
+    raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (tvar,[])], [])
   | SOME (x as (_, sort)) =>
     let
-      val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
+      val (_, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
+      val prop' =
+        fold (fn _ => Term.dest_comb #> #2)
+          (replicate (Thm.nprems_of thm' - Thm.nprems_of thm) ()) (Thm.prop_of thm')
+      val (tyenv, _) = Pattern.first_order_match thy ((prop', Thm.prop_of thm))
+        (Vartab.empty, Vartab.empty)
+      val tyenv_list = tyenv |> Vartab.dest
+        |> map (fn (x, (s, TVar (x', _))) =>
+          ((x, s), Thm.ctyp_of (Context.proof_of context) (TVar(x', s))))
+      val thm'' = Drule.instantiate_normalize (tyenv_list, []) thm'
+      val varify_const =
+        apsnd (subst_TFree "'a" (TVar (tvar, @{sort type}))) #> Const #> Thm.global_cterm_of thy
       val consts = params_of_sort thy sort
-        |> map (apsnd (subst_TFree "'a" tvar) #> Const #> Thm.global_cterm_of thy)
+        |> map varify_const
     in
-      fold Unoverloading.unoverload consts thm'
+      fold Unoverloading.unoverload consts thm''
       |> Raw_Simplifier.norm_hhf (Context.proof_of context)
     end
   end