--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Aug 28 20:06:59 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Aug 28 23:48:46 2014 +0200
@@ -621,11 +621,7 @@
(parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), []))
- | mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits
- | mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
- | mk_horn (neg_lits, pos_lits) =
- mk_aconn AImplies (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
- (foldr1 (uncurry (mk_aconn AOr)) pos_lits)
+ | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits)
fun parse_horn_clause x =
(Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"