--- a/src/HOL/TPTP/atp_export.ML Thu Jul 28 10:42:24 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Thu Jul 28 11:43:45 2011 +0200
@@ -103,8 +103,8 @@
(Formula (ident, Axiom, phi, NONE, NONE)) =
Formula (ident, Lemma, phi, inference infers ident, NONE)
| add_inferences_to_problem_line _ line = line
-val add_inferences_to_problem =
- map o apsnd o map o add_inferences_to_problem_line
+fun add_inferences_to_problem infers =
+ map (apsnd (map (add_inferences_to_problem_line infers)))
fun ident_of_problem_line (Decl (ident, _, _)) = ident
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident