1.1 --- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4      val thy = Proof_Context.theory_of ctxt
     1.5      val t = u
     1.6        |> atp_to_trm
     1.7 -      |> infer_formula_types ctxt
     1.8 +      |> singleton (infer_formula_types ctxt)
     1.9        |> HOLogic.mk_Trueprop
    1.10    in
    1.11      (name, role, t, rule, deps)