src/HOL/ex/tptp_export.ML
changeset 42937 cabb3a947894
parent 42881 dbdfe2d5b6ab
child 42939 0134d6650092
--- a/src/HOL/ex/tptp_export.ML	Sat May 21 11:31:59 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Sun May 22 14:49:35 2011 +0200
@@ -114,7 +114,7 @@
       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
+      ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem
     val _ = app (File.append path) ss
   in () end