# HG changeset patch
# User blanchet
# Date 1308225035 -7200
# Node ID dcbedaf6f80c4f4f1f8161769e2b252ba5ec0d15
# Parent  926bfe067a32bb5c73ac08297c21fdd3e7ceaa00
added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users

diff -r 926bfe067a32 -r dcbedaf6f80c src/HOL/Tools/ATP/atp_problem.ML
--- 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)