# HG changeset patch
# User haftmann
# Date 1168417704 -3600
# Node ID 792c18b8f214bf76e69ad737d01c4cd0ffeeed72
# Parent  2b8909d9d66a6e733877b243d70c91f91047dbc3
improved case patterns

diff -r 2b8909d9d66a -r 792c18b8f214 src/HOL/Tools/datatype_codegen.ML
--- 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 =