# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID 69f657098a35f928d2878213e29137be300fd3c8
# Parent  72b093caf048636e86d63feb82a9ba30fc9b2214
hack to make LEO-II perform better on TPTP THF problems

diff -r 72b093caf048 -r 69f657098a35 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -1308,8 +1308,10 @@
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (role, t)) =>
           let
+            (* FIXME: The commented-out code is a hack to get decent performance
+               out of LEO-II on the TPTP THF benchmarks. *)
             val role =
-              if is_format_with_defs format andalso
+              if (* is_format_with_defs format andalso *)
                  role <> Conjecture andalso is_legitimate_tptp_def t then
                 Definition
               else