# HG changeset patch
# User haftmann
# Date 1285231165 -7200
# Node ID 7bf0c7f0f24c5be6dab77a68eb7e82a6c7603c55
# Parent  6eb38a00ae47bc3e4e8716254eb62b0e5dd74b79# Parent  64fdbee6713541dfaf79527baa488ea705c23e67
merged

diff -r 64fdbee67135 -r 7bf0c7f0f24c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 23 10:37:28 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 23 10:39:25 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")