src/Tools/code/code_thingol.ML
changeset 28708 a1a436f09ec6
parent 28706 3fef773ae6b1
child 28724 4656aacba2bc
     1.1 --- a/src/Tools/code/code_thingol.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/Tools/code/code_thingol.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -667,6 +667,11 @@
     1.4        | is_undefined _ = false;
     1.5      fun mk_case (co, n) t =
     1.6        let
     1.7 +        val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
     1.8 +          else error ("Non-constructor " ^ quote co
     1.9 +            ^ " encountered in case pattern"
    1.10 +            ^ (case thm of NONE => ""
    1.11 +              | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
    1.12          val (vs, body) = Term.strip_abs_eta n t;
    1.13          val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
    1.14        in if is_undefined body then NONE else SOME (selector, body) end;