# HG changeset patch
# User blanchet
# Date 1407164103 -7200
# Node ID 1f0efb4974fc0108f23d4a1ceb008da4894afc80
# Parent  0388026060d18e92a4b2c3a379181df5702a8ca6
tuned comments

diff -r 0388026060d1 -r 1f0efb4974fc src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 04 16:53:09 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 04 16:55:03 2014 +0200
@@ -610,15 +610,13 @@
 
 (**** PARSING OF SPASS OUTPUT ****)
 
-(* SPASS returns clause references of the form "x.y". We ignore "y", whose role
-   is not clear anyway. *)
+(* SPASS returns clause references of the form "x.y". We ignore "y". *)
 val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
 
 val parse_spass_annotations =
   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
 
-(* It is not clear why some literals are followed by sequences of stars and/or
-   pluses. We ignore them. *)
+(* We ignore the stars and the pluses that follow literals. *)
 fun parse_decorated_atom x =
   (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
 
@@ -627,7 +625,7 @@
   | 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)
+      (foldr1 (uncurry (mk_aconn AOr)) pos_lits)
 
 fun parse_horn_clause x =
   (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"