src/HOL/Tools/ATP/atp_proof.ML
changeset 58091 ecf5826ba234
parent 58080 42e998248ddc
child 58324 65651cb9d191
--- 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 --| $$ "|" --| $$ "|"