# HG changeset patch
# User blanchet
# Date 1285230841 -7200
# Node ID 6eb38a00ae47bc3e4e8716254eb62b0e5dd74b79
# Parent  ad436fa9fc5b0576628f364d29f7ff436c14c198
make SML/NJ happy

diff -r ad436fa9fc5b -r 6eb38a00ae47 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 23 09:53:52 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 23 10:34:01 2010 +0200
@@ -301,20 +301,21 @@
     mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
                        foldr1 (mk_aconn AOr) pos_lits)
 
-val parse_horn_clause =
-  Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
-    -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
-    -- Scan.repeat parse_decorated_atom
-  >> (mk_horn o apfst (op @))
+fun parse_horn_clause x =
+  (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
+     -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
+     -- Scan.repeat parse_decorated_atom
+   >> (mk_horn o apfst (op @))) x
 
 (* Syntax: <num>[0:<inference><annotations>]
    <atoms> || <atoms> -> <atoms>. *)
-val parse_spass_line =
-  scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
-  >> (fn ((num, deps), u) => Inference ((num, NONE), u, map (rpair NONE) deps))
+fun parse_spass_line x =
+  (scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+     -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
+   >> (fn ((num, deps), u) =>
+          Inference ((num, NONE), u, map (rpair NONE) deps))) x
 
-val parse_line = parse_tstp_line || parse_vampire_line || parse_spass_line
+fun parse_line x = (parse_tstp_line || parse_vampire_line || parse_spass_line) x
 val parse_proof =
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")