# 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: [0:] || -> . *) -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")