--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Dec 18 17:26:31 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Dec 18 17:27:17 2013 +0100
@@ -658,7 +658,7 @@
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
val spass_pirate_format = DFG Polymorphic
-val remote_spass_pirate_config =
+val remote_spass_pirate_config : atp_config =
{exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 17:26:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 17:27:17 2013 +0100
@@ -200,7 +200,7 @@
[[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
Force_Method], [Meson_Method]]
val rewrite_methodss =
- [[Simp_Method, Auto_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
+ [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]]
fun isar_proof_text ctxt isar_proofs