# HG changeset patch
# User panny
# Date 1405294543 -7200
# Node ID 934a54d04a9acd23736ce44ada4b6c5c8a16668d
# Parent  7a2fbd8c1d98d73f64c2bda6f727e518cfe913b1
throw error for bad input

diff -r 7a2fbd8c1d98 -r 934a54d04a9a src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 14 01:22:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 14 01:35:43 2014 +0200
@@ -765,8 +765,10 @@
         matchedsss
       |>> single
     else if member (op =) sels head then
-      ([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
-       matchedsss)
+      (null prems orelse
+       primcorec_error_eqn "premise(s) in selector formula" eqn;
+       ([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt
+           concl], matchedsss))
     else if is_some rhs_opt andalso
         is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
       if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then