src/HOL/Tools/res_axioms.ML

   | apply_depth (Abs(_,_,t)) = apply_depth t
   | apply_depth _ = 0;
 
 fun too_complex t = 
   apply_depth t > max_apply_depth orelse 
-  Meson.too_many_clauses t orelse
+  Meson.too_many_clauses NONE t orelse
   excessive_lambdas_fm [] t;
   
 fun is_strange_thm th =
   case head_of (concl_of th) of
       Const (a,_) => (a <> "Trueprop" andalso a <> "==")