# HG changeset patch
# User blanchet
# Date 1343403273 -7200
# Node ID fabbed3abc1eee9e04b97a1e740b9c51c24695be
# Parent  2aa8bab841d7005b3ce182da2f80c404064fc20f
tweaks in preparation for type encoding evaluation

diff -r 2aa8bab841d7 -r fabbed3abc1e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 27 16:35:02 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 27 17:34:33 2012 +0200
@@ -644,12 +644,11 @@
               fact_override
       in
         if !reconstructor = "sledgehammer_tac" then
-          sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native"
-          ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
-          ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
-          ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
-          ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN
-            ctxt thms
+          sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
+          ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
+          ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
+          ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
+          ORELSE' SMT_Solver.smt_tac ctxt thms
         else if !reconstructor = "smt" then
           SMT_Solver.smt_tac ctxt thms
         else if full then
diff -r 2aa8bab841d7 -r fabbed3abc1e src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jul 27 16:35:02 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jul 27 17:34:33 2012 +0200
@@ -2659,7 +2659,7 @@
                             ? append (map fst cs)))
                (Datatype.get_all thy) []
 
-val app_op_and_predicator_threshold = 50
+val app_op_and_predicator_threshold = 45
 
 fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
                         uncurried_aliases readable_names preproc hyp_ts concl_t
diff -r 2aa8bab841d7 -r fabbed3abc1e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 27 16:35:02 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 27 17:34:33 2012 +0200
@@ -420,7 +420,7 @@
       (0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))),
       (0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
       (0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))),
-      (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
+      (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), "")))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}