1.1 --- a/src/HOL/TPTP/atp_export.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -152,15 +152,15 @@
     1.4  fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
     1.5    let
     1.6      val format = FOF
     1.7 -    val type_enc = type_enc |> type_enc_from_string
     1.8 +    val type_enc = type_enc |> type_enc_from_string Sound
     1.9      val path = file_name |> Path.explode
    1.10      val _ = File.write path ""
    1.11      val facts = facts_of thy
    1.12      val (atp_problem, _, _, _, _, _, _) =
    1.13        facts
    1.14        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
    1.15 -      |> prepare_atp_problem ctxt format Axiom Axiom type_enc Sound true
    1.16 -                             combinatorsN false true [] @{prop False}
    1.17 +      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN
    1.18 +                             false true [] @{prop False}
    1.19      val atp_problem =
    1.20        atp_problem
    1.21        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.3 @@ -21,8 +21,12 @@
     2.4  
     2.5    datatype order = First_Order | Higher_Order
     2.6    datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
     2.7 +  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
     2.8    datatype type_level =
     2.9 -    All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
    2.10 +    All_Types |
    2.11 +    Noninf_Nonmono_Types of soundness |
    2.12 +    Fin_Nonmono_Types |
    2.13 +    Const_Arg_Types |
    2.14      No_Types
    2.15    datatype type_heaviness = Heavyweight | Lightweight
    2.16  
    2.17 @@ -31,8 +35,6 @@
    2.18      Guards of polymorphism * type_level * type_heaviness |
    2.19      Tags of polymorphism * type_level * type_heaviness
    2.20  
    2.21 -  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    2.22 -
    2.23    val no_lambdasN : string
    2.24    val concealedN : string
    2.25    val liftingN : string
    2.26 @@ -84,11 +86,11 @@
    2.27    val atp_irrelevant_consts : string list
    2.28    val atp_schematic_consts_of : term -> typ list Symtab.table
    2.29    val is_locality_global : locality -> bool
    2.30 -  val type_enc_from_string : string -> type_enc
    2.31 +  val type_enc_from_string : soundness -> string -> type_enc
    2.32    val is_type_enc_higher_order : type_enc -> bool
    2.33    val polymorphism_of_type_enc : type_enc -> polymorphism
    2.34    val level_of_type_enc : type_enc -> type_level
    2.35 -  val is_type_enc_virtually_sound : type_enc -> bool
    2.36 +  val is_type_enc_quasi_sound : type_enc -> bool
    2.37    val is_type_enc_fairly_sound : type_enc -> bool
    2.38    val choose_format : format list -> type_enc -> format * type_enc
    2.39    val mk_aconns :
    2.40 @@ -99,7 +101,7 @@
    2.41    val factsN : string
    2.42    val prepare_atp_problem :
    2.43      Proof.context -> format -> formula_kind -> formula_kind -> type_enc
    2.44 -    -> soundness -> bool -> string -> bool -> bool -> term list -> term
    2.45 +    -> bool -> string -> bool -> bool -> term list -> term
    2.46      -> ((string * locality) * term) list
    2.47      -> string problem * string Symtab.table * int * int
    2.48         * (string * locality) list vector * int list * int Symtab.table
    2.49 @@ -527,8 +529,12 @@
    2.50  
    2.51  datatype order = First_Order | Higher_Order
    2.52  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    2.53 +datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    2.54  datatype type_level =
    2.55 -  All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
    2.56 +  All_Types |
    2.57 +  Noninf_Nonmono_Types of soundness |
    2.58 +  Fin_Nonmono_Types |
    2.59 +  Const_Arg_Types |
    2.60    No_Types
    2.61  datatype type_heaviness = Heavyweight | Lightweight
    2.62  
    2.63 @@ -540,7 +546,7 @@
    2.64  fun try_unsuffixes ss s =
    2.65    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    2.66  
    2.67 -fun type_enc_from_string s =
    2.68 +fun type_enc_from_string soundness s =
    2.69    (case try (unprefix "poly_") s of
    2.70       SOME s => (SOME Polymorphic, s)
    2.71     | NONE =>
    2.72 @@ -554,7 +560,7 @@
    2.73            (* "_query" and "_bang" are for the ASCII-challenged Metis and
    2.74               Mirabelle. *)
    2.75            case try_unsuffixes ["?", "_query"] s of
    2.76 -            SOME s => (Noninf_Nonmono_Types, s)
    2.77 +            SOME s => (Noninf_Nonmono_Types soundness, s)
    2.78            | NONE =>
    2.79              case try_unsuffixes ["!", "_bang"] s of
    2.80                SOME s => (Fin_Nonmono_Types, s)
    2.81 @@ -568,8 +574,9 @@
    2.82             ("simple", (NONE, _, Lightweight)) =>
    2.83             Simple_Types (First_Order, level)
    2.84           | ("simple_higher", (NONE, _, Lightweight)) =>
    2.85 -           if level = Noninf_Nonmono_Types then raise Same.SAME
    2.86 -           else Simple_Types (Higher_Order, level)
    2.87 +           (case level of
    2.88 +              Noninf_Nonmono_Types _ => raise Same.SAME
    2.89 +            | _ => Simple_Types (Higher_Order, level))
    2.90           | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
    2.91           | ("tags", (SOME Polymorphic, _, _)) =>
    2.92             Tags (Polymorphic, level, heaviness)
    2.93 @@ -596,15 +603,20 @@
    2.94    | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
    2.95    | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
    2.96  
    2.97 -fun is_type_level_virtually_sound level =
    2.98 -  level = All_Types orelse level = Noninf_Nonmono_Types
    2.99 -val is_type_enc_virtually_sound =
   2.100 -  is_type_level_virtually_sound o level_of_type_enc
   2.101 +fun is_type_level_quasi_sound All_Types = true
   2.102 +  | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
   2.103 +  | is_type_level_quasi_sound _ = false
   2.104 +val is_type_enc_quasi_sound =
   2.105 +  is_type_level_quasi_sound o level_of_type_enc
   2.106  
   2.107  fun is_type_level_fairly_sound level =
   2.108 -  is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
   2.109 +  is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
   2.110  val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
   2.111  
   2.112 +fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
   2.113 +  | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   2.114 +  | is_type_level_monotonicity_based _ = false
   2.115 +
   2.116  fun choose_format formats (Simple_Types (order, level)) =
   2.117      (case find_first is_format_thf formats of
   2.118         SOME format => (format, Simple_Types (order, level))
   2.119 @@ -624,9 +636,6 @@
   2.120                   | _ => type_enc)
   2.121       | format => (format, type_enc))
   2.122  
   2.123 -(* Soundness controls how sound the "quasi-sound" encodings should be. *)
   2.124 -datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
   2.125 -
   2.126  fun lift_lambdas ctxt type_enc =
   2.127    map (close_form o Envir.eta_contract) #> rpair ctxt
   2.128    #-> Lambda_Lifting.lift_lambdas
   2.129 @@ -1072,24 +1081,38 @@
   2.130  
   2.131  (** Finite and infinite type inference **)
   2.132  
   2.133 -fun deep_freeze_atyp (TVar (_, S)) = TFree ("'frozen", S)
   2.134 -  | deep_freeze_atyp T = T
   2.135 -val deep_freeze_type = map_atyps deep_freeze_atyp
   2.136 +(* These types witness that the type classes they belong to allow infinite
   2.137 +   models and hence that any types with these type classes is monotonic. *)
   2.138 +val known_infinite_types =
   2.139 +  [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
   2.140 +
   2.141 +fun is_type_infinite ctxt soundness locality T =
   2.142 +  (* Unlike virtually any other polymorphic fact whose type variables can be
   2.143 +     instantiated by a known infinite type, extensionality actually encodes a
   2.144 +     cardinality constraints. *)
   2.145 +  soundness <> Sound andalso
   2.146 +  is_type_surely_infinite ctxt
   2.147 +      (if soundness = Unsound andalso locality <> Extensionality then
   2.148 +         known_infinite_types
   2.149 +       else
   2.150 +         []) T
   2.151  
   2.152  (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   2.153     dangerous because their "exhaust" properties can easily lead to unsound ATP
   2.154     proofs. On the other hand, all HOL infinite types can be given the same
   2.155     models in first-order logic (via Löwenheim-Skolem). *)
   2.156  
   2.157 -fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
   2.158 -    exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
   2.159 -  | should_encode_type _ _ All_Types _ = true
   2.160 -  | should_encode_type ctxt _ Fin_Nonmono_Types T =
   2.161 +fun should_encode_type _ _ All_Types _ = true
   2.162 +  | should_encode_type ctxt nonmono_Ts (Noninf_Nonmono_Types soundness) T =
   2.163 +    exists (curry (type_instance ctxt) T) nonmono_Ts andalso
   2.164 +    not (is_type_infinite ctxt soundness General T)
   2.165 +  | should_encode_type ctxt nonmono_Ts Fin_Nonmono_Types T =
   2.166 +    exists (curry (type_instance ctxt) T) nonmono_Ts andalso
   2.167      is_type_surely_finite ctxt T
   2.168    | should_encode_type _ _ _ _ = false
   2.169  
   2.170 -fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
   2.171 -                             should_predicate_on_var T =
   2.172 +fun should_predicate_on_type ctxt nonmono_Ts
   2.173 +        (Guards (_, level, heaviness)) should_predicate_on_var T =
   2.174      (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
   2.175      should_encode_type ctxt nonmono_Ts level T
   2.176    | should_predicate_on_type _ _ _ _ _ = false
   2.177 @@ -1105,19 +1128,13 @@
   2.178    Elsewhere
   2.179  
   2.180  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   2.181 -  | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
   2.182 +  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site
   2.183                           u T =
   2.184      (case heaviness of
   2.185         Heavyweight => should_encode_type ctxt nonmono_Ts level T
   2.186       | Lightweight =>
   2.187         case (site, is_var_or_bound_var u) of
   2.188 -         (Eq_Arg pos, true) =>
   2.189 -         (* The first disjunct prevents a subtle soundness issue explained in
   2.190 -            Blanchette's Ph.D. thesis. (FIXME?) *)
   2.191 -         (pos <> SOME false andalso poly = Polymorphic andalso
   2.192 -          level <> All_Types andalso heaviness = Lightweight andalso
   2.193 -          exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
   2.194 -         should_encode_type ctxt nonmono_Ts level T
   2.195 +         (Eq_Arg _, true) => should_encode_type ctxt nonmono_Ts level T
   2.196         | _ => false)
   2.197    | should_tag_with_type _ _ _ _ _ _ = false
   2.198  
   2.199 @@ -1768,45 +1785,34 @@
   2.200                | _ => fold add_undefined_const (var_types ())))
   2.201    end
   2.202  
   2.203 -(* These types witness that the type classes they belong to allow infinite
   2.204 -   models and hence that any types with these type classes is monotonic. *)
   2.205 -val known_infinite_types =
   2.206 -  [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
   2.207 -
   2.208  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
   2.209     out with monotonicity" paper presented at CADE 2011. *)
   2.210 -fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
   2.211 -  | add_iterm_nonmonotonic_types ctxt level soundness locality _
   2.212 +fun add_iterm_nonmonotonic_types _ _ _ (SOME false) _ = I
   2.213 +  | add_iterm_nonmonotonic_types ctxt level locality _
   2.214          (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
   2.215      (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
   2.216       (case level of
   2.217 -        Noninf_Nonmono_Types =>
   2.218 -        not (is_locality_global locality) orelse
   2.219 -        (* Unlike virtually any other polymorphic fact whose type variables can
   2.220 -           be instantiated by a known infinite type, extensionality actually
   2.221 -           encodes a cardinality constraints. *)
   2.222 -        not (soundness <> Sound andalso
   2.223 -             is_type_surely_infinite ctxt
   2.224 -                 (if locality = Extensionality orelse
   2.225 -                     soundness = Sound_Modulo_Infiniteness then
   2.226 -                    []
   2.227 -                  else
   2.228 -                    known_infinite_types) T)
   2.229 +        Noninf_Nonmono_Types soundness =>
   2.230 +        (* The second conjunct about globality is not strictly necessary, but it
   2.231 +           helps prevent finding proofs that are only sound "modulo
   2.232 +           infiniteness". For example, if the conjecture is
   2.233 +           "EX x y::nat. x ~= y", its untyped negation "ALL x y. x = y" would
   2.234 +           lead to a nonsensical proof that we can't replay. *)
   2.235 +        not (is_type_infinite ctxt soundness locality T
   2.236 +             (* andalso is_locality_global locality *))
   2.237        | Fin_Nonmono_Types => is_type_surely_finite ctxt T
   2.238 -      | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
   2.239 -  | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
   2.240 -fun add_fact_nonmonotonic_types ctxt level soundness
   2.241 +      | _ => true)) ? insert_type ctxt I T
   2.242 +  | add_iterm_nonmonotonic_types _ _ _ _ _ = I
   2.243 +fun add_fact_nonmonotonic_types ctxt level
   2.244          ({kind, locality, iformula, ...} : translated_formula) =
   2.245    formula_fold (SOME (kind <> Conjecture))
   2.246 -               (add_iterm_nonmonotonic_types ctxt level soundness locality)
   2.247 -               iformula
   2.248 -fun nonmonotonic_types_for_facts ctxt type_enc soundness facts =
   2.249 +               (add_iterm_nonmonotonic_types ctxt level locality) iformula
   2.250 +fun nonmonotonic_types_for_facts ctxt type_enc facts =
   2.251    let val level = level_of_type_enc type_enc in
   2.252 -    if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
   2.253 -      [] |> fold (add_fact_nonmonotonic_types ctxt level soundness) facts
   2.254 +    if is_type_level_monotonicity_based level then
   2.255 +      [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
   2.256           (* We must add "bool" in case the helper "True_or_False" is added
   2.257 -            later. In addition, several places in the code rely on the list of
   2.258 -            nonmonotonic types not being empty. (FIXME?) *)
   2.259 +            later. *)
   2.260           |> insert_type ctxt I @{typ bool}
   2.261      else
   2.262        []
   2.263 @@ -2003,7 +2009,7 @@
   2.264  fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
   2.265      poly <> Mangled_Monomorphic andalso
   2.266      ((level = All_Types andalso heaviness = Lightweight) orelse
   2.267 -     level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
   2.268 +     is_type_level_monotonicity_based level)
   2.269    | needs_type_tag_idempotence _ = false
   2.270  
   2.271  fun offset_of_heading_in_problem _ [] j = j
   2.272 @@ -2022,8 +2028,8 @@
   2.273  
   2.274  val explicit_apply = NONE (* for experiments *)
   2.275  
   2.276 -fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc soundness
   2.277 -        exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
   2.278 +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
   2.279 +        lambda_trans readable_names preproc hyp_ts concl_t facts =
   2.280    let
   2.281      val (format, type_enc) = choose_format [format] type_enc
   2.282      val lambda_trans =
   2.283 @@ -2057,8 +2063,7 @@
   2.284        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   2.285                           hyp_ts concl_t facts
   2.286      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
   2.287 -    val nonmono_Ts =
   2.288 -      conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc soundness
   2.289 +    val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc
   2.290      val repair = repair_fact ctxt format type_enc sym_tab
   2.291      val (conjs, facts) = (conjs, facts) |> pairself (map repair)
   2.292      val repaired_sym_tab =

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     3.3 @@ -167,7 +167,7 @@
     3.4  (* Function to generate metis clauses, including comb and type clauses *)
     3.5  fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
     3.6    let
     3.7 -    val type_enc = type_enc_from_string type_enc
     3.8 +    val type_enc = type_enc_from_string Sound type_enc
     3.9      val (conj_clauses, fact_clauses) =
    3.10        if polymorphism_of_type_enc type_enc = Polymorphic then
    3.11          (conj_clauses, fact_clauses)
    3.12 @@ -196,8 +196,8 @@
    3.13        tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
    3.14      *)
    3.15      val (atp_problem, _, _, _, _, _, sym_tab) =
    3.16 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc Sound false
    3.17 -                          no_lambdasN false false [] @{prop False} props
    3.18 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN
    3.19 +                          false false [] @{prop False} props
    3.20      (*
    3.21      val _ = tracing ("ATP PROBLEM: " ^
    3.22                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 22 15:02:45 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 22 15:02:45 2011 +0200
     4.3 @@ -131,7 +131,7 @@
     4.4      (name, value)
     4.5    else if is_prover_list ctxt name andalso null value then
     4.6      ("provers", [name])
     4.7 -  else if can type_enc_from_string name andalso null value then
     4.8 +  else if can (type_enc_from_string Sound) name andalso null value then
     4.9      ("type_enc", [name])
    4.10    else
    4.11      error ("Unknown parameter: " ^ quote name ^ ".")
    4.12 @@ -269,7 +269,7 @@
    4.13          NONE
    4.14        else case lookup_string "type_enc" of
    4.15          "smart" => NONE
    4.16 -      | s => SOME (type_enc_from_string s)
    4.17 +      | s => (type_enc_from_string Sound s; SOME s)
    4.18      val sound = mode = Auto_Try orelse lookup_bool "sound"
    4.19      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    4.20      val max_relevant = lookup_option lookup_int "max_relevant"

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Aug 22 15:02:45 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Aug 22 15:02:45 2011 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4       overlord: bool,
     5.5       blocking: bool,
     5.6       provers: string list,
     5.7 -     type_enc: type_enc option,
     5.8 +     type_enc: string option,
     5.9       sound: bool,
    5.10       relevance_thresholds: real * real,
    5.11       max_relevant: int option,
    5.12 @@ -291,7 +291,7 @@
    5.13     overlord: bool,
    5.14     blocking: bool,
    5.15     provers: string list,
    5.16 -   type_enc: type_enc option,
    5.17 +   type_enc: string option,
    5.18     sound: bool,
    5.19     relevance_thresholds: real * real,
    5.20     max_relevant: int option,
    5.21 @@ -512,11 +512,10 @@
    5.22     them each time. *)
    5.23  val atp_important_message_keep_quotient = 10
    5.24  
    5.25 -fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
    5.26 -  (case type_enc_opt of
    5.27 -     SOME ts => ts
    5.28 -   | NONE => type_enc_from_string best_type_enc)
    5.29 -  |> choose_format formats
    5.30 +fun choose_format_and_type_enc soundness best_type_enc formats =
    5.31 +  the_default best_type_enc
    5.32 +  #> type_enc_from_string soundness
    5.33 +  #> choose_format formats
    5.34  
    5.35  val metis_minimize_max_time = seconds 2.0
    5.36  
    5.37 @@ -616,8 +615,17 @@
    5.38                  val num_facts =
    5.39                    length facts |> is_none max_relevant
    5.40                                    ? Integer.min best_max_relevant
    5.41 +                val soundness =
    5.42 +                  if sound then
    5.43 +                    if Config.get ctxt atp_sound_modulo_infiniteness then
    5.44 +                      Sound_Modulo_Infiniteness
    5.45 +                    else
    5.46 +                      Sound
    5.47 +                  else
    5.48 +                    Unsound
    5.49                  val (format, type_enc) =
    5.50 -                  choose_format_and_type_enc best_type_enc formats type_enc
    5.51 +                  choose_format_and_type_enc soundness best_type_enc formats
    5.52 +                                             type_enc
    5.53                  val fairly_sound = is_type_enc_fairly_sound type_enc
    5.54                  val facts =
    5.55                    facts |> map untranslated_fact
    5.56 @@ -646,19 +654,10 @@
    5.57                      |> Output.urgent_message
    5.58                    else
    5.59                      ()
    5.60 -                val soundness =
    5.61 -                  if sound then
    5.62 -                    if Config.get ctxt atp_sound_modulo_infiniteness then
    5.63 -                      Sound_Modulo_Infiniteness
    5.64 -                    else
    5.65 -                      Sound
    5.66 -                  else
    5.67 -                    Unsound
    5.68                  val (atp_problem, pool, conjecture_offset, facts_offset,
    5.69                       fact_names, typed_helpers, sym_tab) =
    5.70                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    5.71 -                      type_enc soundness false
    5.72 -                      (Config.get ctxt atp_lambda_translation)
    5.73 +                      type_enc false (Config.get ctxt atp_lambda_translation)
    5.74                        (Config.get ctxt atp_readable_names) true hyp_ts concl_t
    5.75                        facts
    5.76                  fun weights () = atp_problem_weights atp_problem
    5.77 @@ -706,7 +705,7 @@
    5.78                          conjecture_shape facts_offset fact_names atp_proof
    5.79                      |> Option.map (fn facts =>
    5.80                             UnsoundProof
    5.81 -                               (if is_type_enc_virtually_sound type_enc then
    5.82 +                               (if is_type_enc_quasi_sound type_enc then
    5.83                                    SOME sound
    5.84                                  else
    5.85                                    NONE, facts |> sort string_ord))