src/HOL/Tools/datatype_abs_proofs.ML

   let
     val _ = writeln "Constructing primrec combinators...";
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
+    val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
 
     val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     val big_rec_name' = (space_implode "_" new_type_names) ^ "_rec_set";
     val rec_set_names = map (Sign.full_name (sign_of thy))
       (if length descr' = 1 then [big_rec_name'] else
         (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
           (1 upto (length descr'))));
 
-    val rec_result_Ts = map (fn (i, _) =>
-      TFree ("'t" ^ (string_of_int (i + 1)), HOLogic.termS)) descr';
+    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
+      replicate (length descr') HOLogic.termS);
 
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
           val recs = filter is_rec_type cargs;

   let
     val _ = writeln "Proving characteristic theorems for case combinators...";
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
+    val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
+    val T' = TFree (variant used "'t", HOLogic.termS);
 
     val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val free = TFree ("'t", HOLogic.termS);
-        val Ts' = replicate (length (filter is_rec_type cargs)) free
-      in Const ("arbitrary", Ts @ Ts' ---> free)
+        val Ts' = replicate (length (filter is_rec_type cargs)) T'
+      in Const ("arbitrary", Ts @ Ts' ---> T')
       end) constrs) descr';
 
     val case_names = map (fn s =>
       Sign.full_name (sign_of thy) (s ^ "_case")) new_type_names;
 
     (* define case combinators via primrec combinators *)
 
     val (case_defs, thy2) = foldl (fn ((defs, thy),
       ((((i, (_, _, constrs)), T), name), recname)) =>
         let
-          val T' = TFree ("'t", HOLogic.termS);
-
           val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
             let
               val Ts = map (typ_of_dtyp descr' sorts) cargs;
               val Ts' = Ts @ (replicate (length (filter is_rec_type cargs)) T');
               val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));