# HG changeset patch
# User blanchet
# Date 1285142559 -7200
# Node ID ae2c3059f8cc05ccbe98f850014c9b4814bf4112
# Parent  922634ecdda4447346f296634c548704868864e8
make SML/NJ happier

diff -r 922634ecdda4 -r ae2c3059f8cc src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Sep 21 14:42:29 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 22 10:02:39 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