src/HOL/Tools/ATP/atp_waldmeister.ML

--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -181,7 +181,7 @@
     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)