Package now chooses type variable names more carefully to
avoid clashes with user-supplied type variable names.

--- 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;

--- a/src/HOL/Tools/datatype_package.ML	Fri Sep 25 16:21:56 1998 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sat Sep 26 16:13:05 1998 +0200
@@ -252,6 +252,7 @@
   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 _ = writeln ("Adding axioms for datatype(s) " ^ commas new_type_names);
@@ -265,8 +266,8 @@
         (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
           (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
 
-    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) =>
@@ -287,7 +288,7 @@
       map (fn i => big_size_name ^ "_" ^ string_of_int i)
         (1 upto length (flat (tl descr)));
 
-    val freeT = TFree ("'t", HOLogic.termS);
+    val freeT = TFree (variant used "'t", HOLogic.termS);
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let val Ts = map (typ_of_dtyp descr' sorts) cargs
@@ -349,7 +350,6 @@
     (**** introduction of axioms ****)
 
     val (thy3, inject) = thy2 |>
-      Theory.add_path (space_implode "_" new_type_names) |>
       PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
       add_and_get_axiomss "inject" new_type_names
         (DatatypeProp.make_injs descr sorts);

--- 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) =