src/HOL/Tools/Function/fundef_datatype.ML

                                        
       val _ = if not (null gs) then err "Conditional equations" else ()
       val _ = map check_constr_pattern args
                   
                   (* just count occurrences to check linearity *)
-      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs
+      val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
               then err "Nonlinear patterns" else ()
     in
       ()
     end