1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  (* Function to generate metis clauses, including comb and type clauses *)
     1.5  fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
     1.6    let
     1.7 -    val type_enc = type_enc_from_string Sound type_enc
     1.8 +    val type_enc = type_enc_from_string Unsound type_enc
     1.9      val (conj_clauses, fact_clauses) =
    1.10        if polymorphism_of_type_enc type_enc = Polymorphic then
    1.11          (conj_clauses, fact_clauses)
    1.12 @@ -202,7 +202,7 @@
    1.13      val _ = tracing ("ATP PROBLEM: " ^
    1.14                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
    1.15      *)
    1.16 -    (* "rev" is for compatibility *)
    1.17 +    (* "rev" is for compatibility. *)
    1.18      val axioms =
    1.19        atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
    1.20                    |> rev