# HG changeset patch
# User blanchet
# Date 1272555068 -7200
# Node ID c6c2661bf08ede50926854050e69819ecadbc0bd
# Parent  f91c7198281110151244aa1c581ae10dd5bf4ad3
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation

diff -r f91c71982811 -r c6c2661bf08e src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 13:41:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 17:31:08 2010 +0200
@@ -186,7 +186,7 @@
 (* It is not clear why some literals are followed by sequences of stars. We
    ignore them. *)
 fun parse_starred_predicate_term pool =
-  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
+  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
 
 fun parse_horn_clause pool =
   Scan.repeat (parse_starred_predicate_term pool) --| $$ "|" --| $$ "|"