# HG changeset patch
# User blanchet
# Date 1347295827 -7200
# Node ID 059aa3088ae33a39fb9382bed3669904b1e3094f
# Parent  9059e0dbdbc1a20d3abe9211258ee8f96dcd16ea
sanity check

diff -r 9059e0dbdbc1 -r 059aa3088ae3 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 18:29:55 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 18:50:27 2012 +0200
@@ -193,6 +193,11 @@
 
     fun sel_spec b proto_sels =
       let
+        val _ =
+          (case duplicates (op =) (map fst proto_sels) of
+             k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
+               " for constructor " ^ quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
+           | [] => ())
         val T =
           (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
             [T] => T