1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Jul 26 14:53:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Jul 26 14:53:00 2011 +0200
     1.3 @@ -197,8 +197,7 @@
     1.4      *)
     1.5      val (atp_problem, _, _, _, _, _, sym_tab) =
     1.6        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
     1.7 -                          (rpair [] o map (introduce_combinators ctxt))
     1.8 -                          false false [] @{prop False} props
     1.9 +                          (rpair []) false false [] @{prop False} props
    1.10      (*
    1.11      val _ = tracing ("ATP PROBLEM: " ^
    1.12                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))