src/HOL/Tools/ATP/atp_problem.ML

                if is_function_type ty then SOME (ary sym ty) else NONE
              | _ => NONE)
       |> commas |> enclose "functions [" "]."
     val pred_aries =
       filt (fn Decl (_, sym, ty) =>
-               if is_nontrivial_predicate_type ty then SOME (ary sym ty)
-               else NONE
+               if is_predicate_type ty then SOME (ary sym ty) else NONE
              | _ => NONE)
       |> commas |> enclose "predicates [" "]."
     fun sorts () =
       filt (fn Decl (_, sym, AType (s, [])) =>
                if s = tptp_type_of_types then SOME sym else NONE

       filt (fn Decl (_, sym, ty) =>
                if is_function_type ty then SOME (fun_typ sym ty) else NONE
              | _ => NONE)
     fun pred_sigs () =
       filt (fn Decl (_, sym, ty) =>
-               if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
+               if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
+               else NONE
              | _ => NONE)
     val decls = if sorted then func_sigs () @ pred_sigs () else []
     val axioms = filt (formula (curry (op <>) Conjecture))
     val conjs = filt (formula (curry (op =) Conjecture))
     fun list_of _ [] = []