added undefined in cases
authorhaftmann
Wed Jan 10 08:58:35 2007 +0100 (2007-01-10)
changeset 220512b8909d9d66a
parent 22050 859e5784c58c
child 22052 792c18b8f214
added undefined in cases
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jan 09 19:09:01 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jan 10 08:58:35 2007 +0100
     1.3 @@ -336,12 +336,14 @@
     1.4      val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     1.5      val (ts', t) = split_last (ts @ map Free abs);
     1.6      val (tys', sty) = split_last tys;
     1.7 -    fun dest_case _ (Const ("undefined", _)) = NONE
     1.8 -      | dest_case ((c, tys_decl), ty) t =
     1.9 -          let
    1.10 -            val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
    1.11 -            val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
    1.12 -          in SOME (c', t') end;
    1.13 +    fun dest_case ((c, tys_decl), ty) t =
    1.14 +      let
    1.15 +        val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
    1.16 +        val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
    1.17 +      in case t'
    1.18 +       of Const ("undefined", _) => NONE
    1.19 +        | _ => SOME (c', t')
    1.20 +      end;
    1.21    in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
    1.22  
    1.23  fun dest_case_expr thy t =