add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula

--- 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