Eliminated DatatypeAux.dest_TFree to avoid clashes
with Term.dest_TFree.

--- a/src/HOL/Tools/datatype_aux.ML	Thu Jan 10 19:10:37 2008 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Thu Jan 10 19:18:14 2008 +0100
@@ -53,7 +53,6 @@
   val strip_dtyp : dtyp -> dtyp list * dtyp
   val body_index : dtyp -> int
   val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
-  val dest_TFree : typ -> string
   val get_nonrec_types : descr -> (string * sort) list -> typ list
   val get_branching_types : descr -> (string * sort) list -> typ list
   val get_arities : descr -> int list
@@ -227,8 +226,6 @@
 fun mk_fun_dtyp [] U = U
   | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
 
-fun dest_TFree (TFree (n, _)) = n;
-
 fun name_of_typ (Type (s, Ts)) =
       let val s' = Sign.base_name s
       in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
@@ -241,7 +238,7 @@
   | dtyp_of_typ new_dts (Type (tname, Ts)) =
       (case AList.lookup (op =) new_dts tname of
          NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
-       | SOME vs => if map (try dest_TFree) Ts = map SOME vs then
+       | SOME vs => if map (try (fst o dest_TFree)) Ts = map SOME vs then
              DtRec (find_index (curry op = tname o fst) new_dts)
            else error ("Illegal occurrence of recursive type " ^ tname));
 

--- a/src/HOL/Tools/datatype_package.ML	Thu Jan 10 19:10:37 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Jan 10 19:18:14 2008 +0100
@@ -725,7 +725,7 @@
       Sign.string_of_term thy1 t);
 
     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
-          ((tname, map dest_TFree Ts) handle TERM _ => err t)
+          ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
       | get_typ t = err t;
 
     val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));