# HG changeset patch
# User haftmann
# Date 1168415915 -3600
# Node ID 2b8909d9d66a6e733877b243d70c91f91047dbc3
# Parent  859e5784c58c8fc287cc93d528118d8533205f15
added undefined in cases

diff -r 859e5784c58c -r 2b8909d9d66a src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Jan 09 19:09:01 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jan 10 08:58:35 2007 +0100
@@ -336,12 +336,14 @@
     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 _ (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;
+    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 case t'
+       of Const ("undefined", _) => NONE
+        | _ => SOME (c', t')
+      end;
   in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
 
 fun dest_case_expr thy t =