src/HOL/Tools/datatype_prop.ML
changeset 5578 7de426cf179c
parent 5177 0d3a168e4d44
child 5695 898429dbb162
--- a/src/HOL/Tools/datatype_prop.ML	Fri Sep 25 16:21:56 1998 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Sat Sep 26 16:13:05 1998 +0200
@@ -166,9 +166,10 @@
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
+    val used = foldr add_typ_tfree_names (recTs, []);
 
-    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) =>
@@ -218,8 +219,9 @@
   let
     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 ("'t", HOLogic.termS);
+    val T' = TFree (variant used "'t", HOLogic.termS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -325,8 +327,9 @@
   let
     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 ("'t", HOLogic.termS);
+    val T' = TFree (variant used' "'t", HOLogic.termS);
     val P = Free ("P", T' --> HOLogic.boolT);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =