--- 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
@@ -196,7 +196,7 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc Sound false
no_lambdasN false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^