# HG changeset patch
# User panny
# Date 1398945929 -7200
# Node ID 8a87502c7da36e729325708c5e9e6c91b97ef7a8
# Parent  38eaaa54cd6ab176115d52d7b3c6054a31a23f19
add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula

diff -r 38eaaa54cd6a -r 8a87502c7da3 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu May 01 10:02:33 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu May 01 14:05:29 2014 +0200
@@ -758,6 +758,7 @@
   in
     if member (op =) discs head orelse
         is_some rhs_opt andalso
+          member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso
           member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
       dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
         matchedsss