     1.1 --- a/src/HOL/TPTP/atp_export.ML	Thu Jan 19 21:37:12 2012 +0100
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Thu Jan 19 21:37:12 2012 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  
     1.5  fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name =
     1.6    let
     1.7 -    val type_enc = type_enc |> type_enc_from_string Sound
     1.8 +    val type_enc = type_enc |> type_enc_from_string Strict
     1.9                              |> adjust_type_enc format
    1.10      val mono = polymorphism_of_type_enc type_enc <> Polymorphic
    1.11      val path = file_name |> Path.explode
changeset 47129	e2e52c7d25c9
parent 46422	a62c7a21f4ab
child 47148	0b8b73b49848