--- 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 **)