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.
removed too strict checks
authorblanchet
Thu, 05 Mar 2015 13:44:41 +0100
changeset 59608 e41ac095f99d
parent 59607 a93592aedce4
child 59609 7892ffd1c39d
removed too strict checks
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 12:32:11 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 13:44:41 2015 +0100
@@ -809,13 +809,11 @@
        (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
-      (check_num_args ();
-       dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
+      (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
          matchedsss
        |>> single)
     else if member (op =) sels head then
       (null prems orelse error_at ctxt [eqn] "Unexpected condition in selector formula";
-       check_num_args ();
        ([dissect_coeqn_sel ctxt 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 is_free_in fun_names head then
isabelle