# HG changeset patch
# User blanchet
# Date 1272470167 -7200
# Node ID d29617bcc1fbfe746599edfbf1c46e7c73818af7
# Parent  a8a6d7172c8c3d17264678ecee00e4c3ec52a63a
properly extract SPASS proof

diff -r a8a6d7172c8c -r d29617bcc1fb src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Apr 28 17:47:30 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Apr 28 17:56:07 2010 +0200
@@ -70,8 +70,10 @@
   case pairself (find_first (fn s => String.isSubstring s output))
                 (ListPair.unzip delims) of
     (SOME begin_delim, SOME end_delim) =>
-    output |> first_field begin_delim |> the |> snd
-           |> first_field end_delim |> the |> fst
+    (output |> first_field begin_delim |> the |> snd
+            |> first_field end_delim |> the |> fst
+            |> first_field "\n" |> the |> snd
+     handle Option.Option => "")
   | _ => ""
 
 fun extract_proof_and_outcome res_code proof_delims known_failures output =