1.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Dec 03 19:32:26 2019 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Dec 03 16:51:53 2019 +0100
     1.3 @@ -44,6 +44,8 @@
     1.4  fun make_tnames Ts =
     1.5    let
     1.6      fun type_name (TFree (name, _)) = unprefix "'" name
     1.7 +      | type_name (TVar ((name, idx), _)) =
     1.8 +          unprefix "'" name ^ (if idx = 0 then "" else string_of_int idx)
     1.9        | type_name (Type (name, _)) =
    1.10            let val name' = Long_Name.base_name name
    1.11            in if Symbol_Pos.is_identifier name' then name' else "x" end;
    1.12 @@ -259,8 +261,7 @@
    1.13    let
    1.14      val (_, T) = dest_Const c;
    1.15      val Ts = binder_types T;
    1.16 -    val (names, _) =
    1.17 -      fold_map Name.variant (make_tnames (map Logic.unvarifyT_global Ts)) used;
    1.18 +    val (names, _) = fold_map Name.variant (make_tnames Ts) used;
    1.19      val ty = body_type T;
    1.20      val ty_theta = Type.raw_match (ty, colty) Vartab.empty
    1.21        handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);