# HG changeset patch
# User immler
# Date 1528824655 -7200
# Node ID 38961724a017acbdba29f2eee76af157548ab2a7
# Parent  46beee72fb66065283acc9efcf06c4ecffd59a30
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar

diff -r 46beee72fb66 -r 38961724a017 src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 16:21:52 2018 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 19:30:55 2018 +0200
@@ -27,6 +27,18 @@
       List.concat
   in params end
 
+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 ("unoverload_type: 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])
+  in
+    (tvar, thm')
+  end
+
 fun unoverload_type context s thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
@@ -36,7 +48,7 @@
     raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
   | SOME (x as (_, sort)) =>
     let
-      val (tvar, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
+      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)))
     in