1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 27 14:56:26 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 27 14:56:28 2011 +0200
     1.3 @@ -196,8 +196,8 @@
     1.4        tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     1.5      *)
     1.6      val (atp_problem, _, _, _, _, _, sym_tab) =
     1.7 -      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false false
     1.8 -                          [] @{prop False} props
     1.9 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
    1.10 +                          false [] @{prop False} props
    1.11      (*
    1.12      val _ = tracing ("ATP PROBLEM: " ^
    1.13                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))