src/HOL/ex/atp_export.ML
changeset 43224 97906dfd39b7
parent 43223 c9e87dc92d9e
child 43245 cef69d31bfa4
--- a/src/HOL/ex/atp_export.ML	Tue Jun 07 07:04:53 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Tue Jun 07 07:06:24 2011 +0200
@@ -114,8 +114,7 @@
     val infers =
       infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
     val atp_problem = atp_problem |> add_inferences_to_problem infers
-    val ss =
-      ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem
+    val ss = ATP_Problem.tptp_lines_for_atp_problem ATP_Problem.FOF atp_problem
     val _ = app (File.append path) ss
   in () end