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