src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Sep 21 16:56:11 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Sep 21 19:53:50 2014 +0200
@@ -708,9 +708,8 @@
       case results of
           Nonempty (SOME results') =>
             #2 results'
-            |> map (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) =>
+            |> maps (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) =>
                  if inf_name = inference_name then [inf_fmla] else [])
-            |> List.concat
         | _ => []
   in Specific_rule (filename, inference_name, filtered_results) end