src/HOL/Tools/datatype_codegen.ML
changeset 21012 f08574148b7a
parent 20855 9f60d493c8fe
child 21046 fe1db2f991a7
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:46 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:47 2006 +0200
     1.3 @@ -336,8 +336,6 @@
     1.4      val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     1.5      val (ts', t) = split_last (ts @ map Free abs);
     1.6      val (tys', sty) = split_last tys;
     1.7 -    fun freenames_of t = fold_aterms
     1.8 -      (fn Free (v, _) => insert (op =) v | _ => I) t [];
     1.9      fun dest_case ((c, tys_decl), ty) t =
    1.10        let
    1.11          val (vs, t') = Term.strip_abs_eta (length tys_decl) t;