# HG changeset patch
# User blanchet
# Date 1425559481 -3600
# Node ID e41ac095f99d4377a14b9a5bf7af5422ab521695
# Parent  a93592aedce42783d2014397cebf788e1bf90dba
removed too strict checks

diff -r a93592aedce4 -r e41ac095f99d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- 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