src/HOL/Tools/datatype_abs_proofs.ML
changeset 5578 7de426cf179c
parent 5553 ae42b36a50c2
child 5661 6ecb6ea25f19
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 25 16:21:56 1998 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Sep 26 16:13:05 1998 +0200
@@ -103,6 +103,7 @@
 
     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)));
@@ -113,8 +114,8 @@
         (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) =>
@@ -280,14 +281,15 @@
 
     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 =>
@@ -298,8 +300,6 @@
     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;