# HG changeset patch
# User blanchet
# Date 1355793525 -3600
# Node ID 9d2f223ab6d994b15a2a54f9c4a3914a4368315f
# Parent  42f3630a6a0ff29cf16140f65da3a27055b8a0db
catch all parsing errors

diff -r 42f3630a6a0f -r 9d2f223ab6d9 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 18 00:17:37 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 18 02:18:45 2012 +0100
@@ -496,13 +496,13 @@
 fun parse_line problem =
   parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
   || parse_satallax_line
-fun parse_proof problem tstp =
-  tstp |> strip_spaces_except_between_idents
-       |> raw_explode
-       |> Scan.finite Symbol.stopper
-              (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-                              (Scan.repeat1 (parse_line problem))))
-       |> fst
+fun parse_proof problem =
+  strip_spaces_except_between_idents
+  #> raw_explode
+  #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
+         (Scan.finite Symbol.stopper
+                         (Scan.repeat1 (parse_line problem))))
+  #> fst
 
 fun atp_proof_from_tstplike_proof _ "" = []
   | atp_proof_from_tstplike_proof problem tstp =