Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
throw error for bad input
authorpanny
Mon, 14 Jul 2014 01:35:43 +0200
changeset 57550 934a54d04a9a
parent 57549 7a2fbd8c1d98
child 57551 c07bac41c7ab
throw error for bad input
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle