# HG changeset patch
# User blanchet
# Date 1479227980 -3600
# Node ID 233a11ed2dfb437455a497fbdd475e9618273ac7
# Parent  daae191c9344dbf3bfd43ec514295093407be8f9
generalized experimental feature slightly

diff -r daae191c9344 -r 233a11ed2dfb src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Tue Nov 08 13:03:54 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Tue Nov 15 17:39:40 2016 +0100
@@ -185,7 +185,7 @@
     val thy = Proof_Context.theory_of ctxt
     val assm_ths0 = map (Skip_Proof.make_thm thy) assms
     val ((assm_name, _), ctxt) = ctxt
-      |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 2 else 0)
+      |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
       |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
 
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
diff -r daae191c9344 -r 233a11ed2dfb src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Nov 08 13:03:54 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Nov 15 17:39:40 2016 +0100
@@ -1529,7 +1529,7 @@
 val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
 
 fun predicatify completish tm =
-  if completish > 0 then
+  if completish > 1 then
     IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm), fTrue_iconst)
   else
     IApp (predicator_iconst, tm)
@@ -1733,14 +1733,14 @@
       fold (fn ((helper_s, needs_sound), ths) =>
                if (needs_sound andalso not sound) orelse
                   (helper_s <> unmangled_s andalso
-                   (completish < 2 orelse could_specialize)) then
+                   (completish < 3 orelse could_specialize)) then
                  I
                else
                  ths ~~ (1 upto length ths)
                  |> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of))
                  |> make_facts
                  |> union (op = o apply2 #iformula))
-           (if completish >= 2 then completish_helper_table else helper_table)
+           (if completish >= 3 then completish_helper_table else helper_table)
     end
   | NONE => I)
 fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
@@ -2168,7 +2168,7 @@
 fun default_mono level completish =
   {maybe_finite_Ts = [@{typ bool}],
    surely_infinite_Ts = (case level of Nonmono_Types (Strict, _) => [] | _ => known_infinite_types),
-   maybe_nonmono_Ts = [if completish >= 2 then tvar_a else @{typ bool}]}
+   maybe_nonmono_Ts = [if completish >= 3 then tvar_a else @{typ bool}]}
 
 (* This inference is described in section 4 of Blanchette et al., "Encoding
    monomorphic and polymorphic types", TACAS 2013. *)