# HG changeset patch
# User blanchet
# Date 1311684780 -7200
# Node ID c51b4196b5e6d9d7251f009358e3cbbc74aecc0f
# Parent  05ff40b255eb7a5071fbf612a055e27f3140cb5d
tuning -- remove useless function (at this point combinators are already in)

diff -r 05ff40b255eb -r c51b4196b5e6 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Jul 26 14:53:00 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Jul 26 14:53:00 2011 +0200
@@ -197,8 +197,7 @@
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
-                          (rpair [] o map (introduce_combinators ctxt))
-                          false false [] @{prop False} props
+                          (rpair []) false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (tptp_lines_for_atp_problem CNF atp_problem))