--- a/src/HOL/Tools/datatype_codegen.ML Wed Jan 10 08:58:35 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Wed Jan 10 09:28:24 2007 +0100
@@ -333,7 +333,8 @@
fun dest_case_app cs ts tys =
let
- val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
+ val names = (Name.make_context o map fst) (fold Term.add_tfrees ts []);
+ val abs = Name.names names "a" (Library.drop (length ts, tys));
val (ts', t) = split_last (ts @ map Free abs);
val (tys', sty) = split_last tys;
fun dest_case ((c, tys_decl), ty) t =