# HG changeset patch
# User traytel
# Date 1575388313 -3600
# Node ID 54a7ad860a765ecbf13b78ca4fe1e7232eb7984d
# Parent  d411d5c84a4b4fcb841b980ee91aaa5579bb30b1
made internal name generation in case expressions more robust

diff -r d411d5c84a4b -r 54a7ad860a76 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Dec 03 19:32:26 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Dec 03 16:51:53 2019 +0100
@@ -44,6 +44,8 @@
 fun make_tnames Ts =
   let
     fun type_name (TFree (name, _)) = unprefix "'" name
+      | type_name (TVar ((name, idx), _)) =
+          unprefix "'" name ^ (if idx = 0 then "" else string_of_int idx)
       | type_name (Type (name, _)) =
           let val name' = Long_Name.base_name name
           in if Symbol_Pos.is_identifier name' then name' else "x" end;
@@ -259,8 +261,7 @@
   let
     val (_, T) = dest_Const c;
     val Ts = binder_types T;
-    val (names, _) =
-      fold_map Name.variant (make_tnames (map Logic.unvarifyT_global Ts)) used;
+    val (names, _) = fold_map Name.variant (make_tnames Ts) used;
     val ty = body_type T;
     val ty_theta = Type.raw_match (ty, colty) Vartab.empty
       handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);