1.1 --- a/src/HOL/TPTP/atp_export.ML	Thu Jul 28 10:42:24 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Thu Jul 28 11:43:45 2011 +0200
     1.3 @@ -103,8 +103,8 @@
     1.4                                     (Formula (ident, Axiom, phi, NONE, NONE)) =
     1.5      Formula (ident, Lemma, phi, inference infers ident, NONE)
     1.6    | add_inferences_to_problem_line _ line = line
     1.7 -val add_inferences_to_problem =
     1.8 -  map o apsnd o map o add_inferences_to_problem_line
     1.9 +fun add_inferences_to_problem infers =
    1.10 +  map (apsnd (map (add_inferences_to_problem_line infers)))
    1.11  
    1.12  fun ident_of_problem_line (Decl (ident, _, _)) = ident
    1.13    | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident