don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 14 15:14:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 14 15:14:38 2011 +0200
@@ -385,8 +385,9 @@
                  #> map negate_conjecture_line))
   |> (fn problem =>
          let
-           val conjs = problem |> maps snd |> filter is_problem_line_negated
-         in if length conjs = 1 then problem else [] end)
+           val lines = problem |> maps snd
+           val conjs = lines |> filter is_problem_line_negated
+         in if length conjs = 1 andalso conjs <> lines then problem else [] end)
 
 
 (** Symbol declarations **)