improved case patterns
authorhaftmann
Wed Jan 10 09:28:24 2007 +0100 (2007-01-10)
changeset 22052792c18b8f214
parent 22051 2b8909d9d66a
child 22053 4b713f89f8c7
improved case patterns
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jan 10 08:58:35 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jan 10 09:28:24 2007 +0100
     1.3 @@ -333,7 +333,8 @@
     1.4  
     1.5  fun dest_case_app cs ts tys =
     1.6    let
     1.7 -    val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     1.8 +    val names = (Name.make_context o map fst) (fold Term.add_tfrees ts []);
     1.9 +    val abs = Name.names names "a" (Library.drop (length ts, tys));
    1.10      val (ts', t) = split_last (ts @ map Free abs);
    1.11      val (tys', sty) = split_last tys;
    1.12      fun dest_case ((c, tys_decl), ty) t =