src/HOL/Tools/ATP/atp_waldmeister.ML

 fun termify_line ctxt (name, role, AAtom u, rule, deps) =
   let
     val thy = Proof_Context.theory_of ctxt
     val t = u
       |> atp_to_trm
-      |> infer_formula_types ctxt
+      |> singleton (infer_formula_types ctxt)
       |> HOLogic.mk_Trueprop
   in
     (name, role, t, rule, deps)
   end