# HG changeset patch
# User blanchet
# Date 1285056170 -7200
# Node ID 57413334669d492b231a096925af2c9fef0720db
# Parent  48f63a6c7f851f283eb90887a615acb5b46565b6
make SML/NJ happier

diff -r 48f63a6c7f85 -r 57413334669d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Sep 21 02:03:40 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Sep 21 10:02:50 2010 +0200
@@ -215,12 +215,12 @@
    >> ATerm) x
 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
 
-val parse_atom =
-  parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
-  >> (fn (u1, NONE) => AAtom u1
-       | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
-       | (u1, SOME (SOME _, u2)) =>
-         mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))
+fun parse_atom x =
+  (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
+   >> (fn (u1, NONE) => AAtom u1
+        | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
+        | (u1, SOME (SOME _, u2)) =>
+          mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))) x
 
 fun fo_term_head (ATerm (s, _)) = s