added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jun 16 13:50:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jun 16 13:50:35 2011 +0200
@@ -317,6 +317,7 @@
           AConn (c, [opn pos1 phi1, opn pos2 phi2])
         end
       | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)
+      | opn _ phi = phi
   in opn (SOME (not conj)) end
 fun open_formula_line (Formula (ident, kind, phi, source, info)) =
     Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)