# HG changeset patch
# User blanchet
# Date 1315423881 -7200
# Node ID 9e177ffe4745e1ccd87781b306e3d8a8109dff8a
# Parent  0bff1a4228b3037f3fa71cebe6fc81267473e625
smarter explicit apply business

diff -r 0bff1a4228b3 -r 9e177ffe4745 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
@@ -2236,13 +2236,22 @@
 val conjsN = "Conjectures"
 val free_typesN = "Type variables"
 
-val explicit_apply = NONE (* for experiments *)
+val explicit_apply_threshold = 50
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
         lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
+    (* Forcing explicit applications is expensive for polymorphic encodings,
+       because it takes only one existential variable ranging over "'a => 'b" to
+       ruin everything. Hence we do it only if there are few facts. *)
+    val explicit_apply =
+      if polymorphism_of_type_enc type_enc <> Polymorphic orelse
+         length facts <= explicit_apply_threshold then
+        NONE
+      else
+        SOME false
     val lambda_trans =
       if lambda_trans = smartN then
         if is_type_enc_higher_order type_enc then lambdasN else combinatorsN