# HG changeset patch
# User blanchet
# Date 1387384037 -3600
# Node ID c05ed63333023e87e84340eab77cd4b59d6b0b22
# Parent  a77f18378b8fcf4b6285cb67ad6096fcf009b4f9# Parent  9ce867291c76330f48759402265375520e941544
merge

diff -r a77f18378b8f -r c05ed6333302 src/HOL/Tools/ATP/atp_systems.ML
--- 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,
diff -r a77f18378b8f -r c05ed6333302 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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