# HG changeset patch
# User blanchet
# Date 1347291362 -7200
# Node ID 0dc6cf758ed1b348b81f780487307e79d1e19e63
# Parent  b21c03c7a0970585fa54cd5720e0c5f769a2a7b6
prevent inconsistent selector types

diff -r b21c03c7a097 -r 0dc6cf758ed1 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 17:36:02 2012 +0200
@@ -191,9 +191,15 @@
           NONE => mk_undef T Ts
         | SOME (xs, x) => fold_rev Term.lambda xs x) ctr_Tss ks;
 
-    (* TODO: check types of tail of list *)
-    fun sel_spec b (proto_sels as ((_, (_, x)) :: _)) =
-      let val T = fastype_of x in
+    fun sel_spec b proto_sels =
+      let
+        val T =
+          (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
+            [T] => T
+          | T :: T' :: _ => error ("Inconsistent range type for selector " ^
+              quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
+              " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
+      in
         mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v,
           Term.list_comb (mk_case As T, mk_sel_case_args proto_sels T) $ v)
       end;