--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 22 10:30:24 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 22 11:46:28 2010 +0200
@@ -291,8 +291,8 @@
(* It is not clear why some literals are followed by sequences of stars and/or
pluses. We ignore them. *)
-val parse_decorated_atom =
- parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
+fun parse_decorated_atom x =
+ (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
| mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits