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