# HG changeset patch
# User blanchet
# Date 1407154783 -7200
# Node ID b5dc0562c7fbcc3fbe76701c5c8327e5c5d6e85d
# Parent  c1ce4ef23be57f8663561393860485d000228ce2
renamed 'sh_minimize' to 'minimize'; compile;

diff -r c1ce4ef23be5 -r b5dc0562c7fb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 04 13:48:05 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 04 14:19:43 2014 +0200
@@ -23,7 +23,7 @@
 val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*)
 val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
 val isar_proofsK = "isar_proofs" (*: enable Isar proof generation*)
-val sh_minimizeK = "sh_minimize" (*: instruct sledgehammer to run its minimizer*)
+val minimizeK = "minimize" (*: instruct sledgehammer to run its minimizer*)
 
 val check_trivialK = "check_trivial" (*: check if goals are "trivial" (false by default)*)
 val fact_filterK = "fact_filter" (*=STRING: fact filter*)
@@ -349,7 +349,7 @@
 
 fun run_sh prover_name fact_filter type_enc strict max_facts slice
       lam_trans uncurried_aliases e_selection_heuristic term_order force_sos
-      hard_timeout timeout preplay_timeout isar_proofsLST sh_minimizeLST
+      hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST
       max_new_mono_instancesLST max_mono_itersLST dir pos st =
   let
     val thy = Proof.theory_of st
@@ -373,7 +373,7 @@
                   term_order |> the_default I)
             #> (Option.map (Config.put ATP_Systems.force_sos)
                   force_sos |> the_default I))
-    val params as {max_facts, preplay_timeout, ...} =
+    val params as {max_facts, minimize, preplay_timeout, ...} =
       Sledgehammer_Commands.default_params thy
          ([("verbose", "true"),
            ("fact_filter", fact_filter),
@@ -386,7 +386,7 @@
            ("timeout", string_of_int timeout),
            ("preplay_timeout", preplay_timeout)]
           |> isar_proofsLST
-          |> sh_minimizeLST (*don't confuse the two minimization flags*)
+          |> minimizeLST (*don't confuse the two minimization flags*)
           |> max_new_mono_instancesLST
           |> max_mono_itersLST)
     val default_max_facts =
@@ -428,8 +428,8 @@
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     val time_prover = run_time |> Time.toMilliseconds
-    val msg = message (fn () => Sledgehammer.play_one_line_proof preplay_timeout used_facts st' i
-      preferred_methss)
+    val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts
+      st' i preferred_methss)
   in
     (case outcome of
       NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
@@ -471,7 +471,7 @@
     val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
       |> the_default preplay_timeout_default
     val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs"
-    val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
+    val minimizeLST = available_parameter args minimizeK "minimize"
     val max_new_mono_instancesLST =
       available_parameter args max_new_mono_instancesK max_new_mono_instancesK
     val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
@@ -479,7 +479,7 @@
     val (msg, result) =
       run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans
         uncurried_aliases e_selection_heuristic term_order force_sos
-        hard_timeout timeout preplay_timeout isar_proofsLST sh_minimizeLST
+        hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST
         max_new_mono_instancesLST max_mono_itersLST dir pos st
   in
     (case result of