# HG changeset patch
# User blanchet
# Date 1304405536 -7200
# Node ID 6099b85ae48edfb8451157e4ea49c44a02afc3fa
# Parent  59142dbfa3baca326f4e1fd9fe467927c575a86e
make SML/NJ happiest

diff -r 59142dbfa3ba -r 6099b85ae48e src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 03 01:04:03 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 03 08:52:16 2011 +0200
@@ -401,11 +401,13 @@
           Inference ((num, NONE), u, map (rpair NONE) deps))) x
 
 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")
-                            (Scan.repeat1 parse_line)))
-  o raw_explode o strip_spaces_except_between_ident_chars
+fun parse_proof s =
+  s |> strip_spaces_except_between_ident_chars
+    |> raw_explode
+    |> Scan.finite Symbol.stopper
+           (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
+                           (Scan.repeat1 parse_line)))
+    |> fst
 
 fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
 fun clean_up_dependencies _ [] = []