--- 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) --| $$ "|" --| $$ "|"