diff -r 5dcc3c257922 -r 48cc198b9ac5 src/HOL/Tools/datatype_aux.ML
--- 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));