src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:46 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:47 2006 +0200
@@ -336,8 +336,6 @@
     val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     val (ts', t) = split_last (ts @ map Free abs);
     val (tys', sty) = split_last tys;
-    fun freenames_of t = fold_aterms
-      (fn Free (v, _) => insert (op =) v | _ => I) t [];
     fun dest_case ((c, tys_decl), ty) t =
       let
         val (vs, t') = Term.strip_abs_eta (length tys_decl) t;