# 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