--- a/src/HOL/Tools/datatype_codegen.ML Tue Jan 09 19:08:56 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Jan 09 19:08:58 2007 +0100
@@ -336,12 +336,13 @@
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 dest_case ((c, tys_decl), ty) t =
- let
- val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
- val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
- in (c', t') end;
- in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts')) end;
+ fun dest_case _ (Const ("undefined", _)) = NONE
+ | dest_case ((c, tys_decl), ty) t =
+ let
+ val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
+ val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
+ in SOME (c', t') end;
+ in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
fun dest_case_expr thy t =
case strip_comb t