# HG changeset patch # User haftmann # Date 1168366138 -3600 # Node ID ff91fd74bb71c61b410e07236af75ebed82cebc2 # Parent ce84c9887e2dd012c82b101c9eda199b143c0271 handling for "undefined" in case expressions diff -r ce84c9887e2d -r ff91fd74bb71 src/HOL/Tools/datatype_codegen.ML --- 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