changeset 46301 | e2e52c7d25c9 |
parent 45551 | a62c7a21f4ab |
child 46320 | 0b8b73b49848 |
--- a/src/HOL/TPTP/atp_export.ML Thu Jan 19 21:37:12 2012 +0100 +++ b/src/HOL/TPTP/atp_export.ML Thu Jan 19 21:37:12 2012 +0100 @@ -169,7 +169,7 @@ fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name = let - val type_enc = type_enc |> type_enc_from_string Sound + val type_enc = type_enc |> type_enc_from_string Strict |> adjust_type_enc format val mono = polymorphism_of_type_enc type_enc <> Polymorphic val path = file_name |> Path.explode