--- a/src/HOL/ATP.thy Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/ATP.thy Thu Apr 23 15:45:42 2020 +0200
@@ -137,6 +137,5 @@
ML_file \<open>Tools/monomorph.ML\<close>
ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
-ML_file \<open>Tools/ATP/atp_systems.ML\<close>
end
--- a/src/HOL/Sledgehammer.thy Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Apr 23 15:45:42 2020 +0200
@@ -16,6 +16,7 @@
lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
by (erule contrapos_nn) (rule arg_cong)
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 23 15:45:42 2020 +0200
@@ -453,7 +453,7 @@
(InternalError, "Please report this error")] @
known_perl_failures,
prem_role = Conjecture,
- best_slices = fn ctxt =>
+ best_slices = fn _ =>
(* FUDGE *)
[(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
(0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
@@ -499,7 +499,7 @@
val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
val vampire_full_proof_options =
- " --forced_options equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
+ " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
val remote_vampire_command =
"vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"