# HG changeset patch
# User blanchet
# Date 1391112139 -3600
# Node ID 78eb7fab3284cc98f3cd0af95a68751647f74b33
# Parent  b75b52c7cf9443acd4ef7a8049a4aac4e749375e
tuning

diff -r b75b52c7cf94 -r 78eb7fab3284 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 20:39:49 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 21:02:19 2014 +0100
@@ -88,12 +88,12 @@
 
 fun tac_of_method meth type_enc lam_trans ctxt facts =
   (case meth of
-    Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
+    Metis_Method_with_Args => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
   | Meson_Method => Meson.meson_tac ctxt facts
   | _ =>
     Method.insert_tac facts THEN'
     (case meth of
-      Metis_New_Skolem_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt []
+      Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt []
     | Simp_Method => Simplifier.asm_full_simp_tac ctxt
     | Simp_Size_Method =>
       Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
diff -r b75b52c7cf94 -r 78eb7fab3284 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jan 30 20:39:49 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jan 30 21:02:19 2014 +0100
@@ -170,7 +170,7 @@
 
     fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
 
-    fun of_method ls ss Metis_Method = of_metis ls ss
+    fun of_method ls ss Metis_Method_with_Args = of_metis ls ss
       | of_method ls ss meth = using_facts ls ss ^ by_method meth
 
     fun of_byline ind (ls, ss) meth =
@@ -245,7 +245,7 @@
     (* One-step Metis proofs are pointless; better use the one-liner directly. *)
     (case proof of
       Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
-    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
+    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method_with_Args :: _) :: _))]) => ""
     | _ =>
       (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
diff -r b75b52c7cf94 -r 78eb7fab3284 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jan 30 20:39:49 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Thu Jan 30 21:02:19 2014 +0100
@@ -20,7 +20,7 @@
     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
       (facts * proof_method list list)
   and proof_method =
-    Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
+    Metis_Method_with_Args | Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method |
     Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
 
   val no_label : label
@@ -69,7 +69,7 @@
   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
     (facts * proof_method list list)
 and proof_method =
-  Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
+  Metis_Method_with_Args | Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method |
   Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
 
 val no_label = ("", ~1)
diff -r b75b52c7cf94 -r 78eb7fab3284 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 20:39:49 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 21:02:19 2014 +0100
@@ -194,14 +194,14 @@
 
 val arith_methodss =
   [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
-    Metis_Method], [Meson_Method]]
+    Metis_Method_with_Args], [Meson_Method]]
 val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
 val metislike_methodss =
-  [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+  [[Metis_Method_with_Args, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
     Force_Method], [Meson_Method]]
 val rewrite_methodss =
-  [[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]]
+  [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method_with_Args], [Meson_Method]]
+val skolem_methodss = [[Metis_Method_with_Args, Blast_Method], [Metis_Method], [Meson_Method]]
 
 fun isar_proof_text ctxt debug isar_proofs isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =