# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID b529d9501d64686e4cacc900567b9e954db6b5d6
# Parent  30ea62ab4f166cc8f72fd35518baf04fe5ec5b22
prefer the lighter, slightly unsound monotonicity-based encodings for Metis

diff -r 30ea62ab4f16 -r b529d9501d64 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -167,7 +167,7 @@
 (* Function to generate metis clauses, including comb and type clauses *)
 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
   let
-    val type_enc = type_enc_from_string Sound type_enc
+    val type_enc = type_enc_from_string Unsound type_enc
     val (conj_clauses, fact_clauses) =
       if polymorphism_of_type_enc type_enc = Polymorphic then
         (conj_clauses, fact_clauses)
@@ -202,7 +202,7 @@
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
     *)
-    (* "rev" is for compatibility *)
+    (* "rev" is for compatibility. *)
     val axioms =
       atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
                   |> rev