# HG changeset patch
# User blanchet
# Date 1310649278 -7200
# Node ID 0234156d3fbe9c9e96d20f3f8ae1c68567dbd4fc
# Parent  9361c7c930d02ddfd0b3b4a071536e4b84528dc3
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes

diff -r 9361c7c930d0 -r 0234156d3fbe src/HOL/Tools/ATP/atp_problem.ML
--- 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 **)