# HG changeset patch
# User blanchet
# Date 1379709570 -7200
# Node ID 06510d01a07b31a0520b1395c75b34fb2f28b660
# Parent  4d34e267fba9c38474bb97d272b09adcc06f3ecf
hard-coded an obscure option

diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -14,8 +14,7 @@
   type isar_proof = Sledgehammer_Proof.isar_proof
   type preplay_interface = Sledgehammer_Preplay.preplay_interface
 
-  val compress_proof :
-    real -> int -> real -> preplay_interface -> isar_proof -> isar_proof
+  val compress_proof : real -> int -> preplay_interface -> isar_proof -> isar_proof
 end
 
 
@@ -117,16 +116,18 @@
 
 (*** main function ***)
 
+val merge_timeout_slack = 1.2
+
 (* PRE CONDITION: the proof must be labeled canocially, see
    Slegehammer_Proof.relabel_proof_canonically *)
-fun compress_proof isar_compress isar_compress_degree merge_timeout_slack
-  ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface)
+fun compress_proof isar_compress isar_compress_degree
+        ({get_preplay_time, set_preplay_time, preplay_quietly, ...}
+         : preplay_interface)
   proof =
   if isar_compress <= 1.0 then
     proof
   else
   let
-
     val (compress_further : unit -> bool,
          decrement_step_count : unit -> unit) =
       let
diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -94,8 +94,7 @@
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "smart"),
    ("isar_compress", "10"),
-   ("isar_compress_degree", "2"), (* TODO: document; right value?? *)
-   ("merge_timeout_slack", "1.2"), (* TODO: document *)
+   ("isar_compress_degree", "2"), (* TODO: document *)
    ("isar_try0", "true"), (* TODO: document *)
    ("isar_minimize", "true"), (* TODO: document *)
    ("slice", "true"),
@@ -306,7 +305,6 @@
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val isar_compress = Real.max (1.0, lookup_real "isar_compress")
     val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree")
-    val merge_timeout_slack = Real.max (1.0, lookup_real "merge_timeout_slack")
     val isar_try0 = lookup_bool "isar_try0"
     val isar_minimize = lookup_bool "isar_minimize"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
@@ -325,8 +323,7 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
      isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
-     merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
-     isar_minimize = isar_minimize, slice = slice,
+     isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
      expect = expect}
   end
diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -58,8 +58,8 @@
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_enc, strict, lam_trans,
                  uncurried_aliases, isar_proofs, isar_compress,
-                 isar_compress_degree, merge_timeout_slack, isar_try0,
-                 isar_minimize, preplay_timeout, ...} : params)
+                 isar_compress_degree, isar_try0, isar_minimize,
+                 preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
     val _ =
@@ -81,11 +81,9 @@
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances,
        isar_proofs = isar_proofs, isar_compress = isar_compress,
-       isar_compress_degree = isar_compress_degree,
-       merge_timeout_slack = merge_timeout_slack,
-       isar_try0 = isar_try0, isar_minimize = isar_minimize,
-       slice = false, minimize = SOME false, timeout = timeout,
-       preplay_timeout = preplay_timeout, expect = ""}
+       isar_compress_degree = isar_compress_degree, isar_try0 = isar_try0,
+       isar_minimize = isar_minimize, slice = false, minimize = SOME false,
+       timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
@@ -255,9 +253,8 @@
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
          fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
-         isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0,
-         isar_minimize, slice, minimize, timeout, preplay_timeout, expect} :
-         params) =
+         isar_compress, isar_compress_degree, isar_try0, isar_minimize, slice,
+         minimize, timeout, preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       case AList.lookup (op =) override_params name of
@@ -275,9 +272,9 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
      isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
-     merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
-     isar_minimize = isar_minimize, slice = slice, minimize = minimize,
-     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice,
+     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name
diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -37,7 +37,6 @@
      isar_proofs : bool option,
      isar_compress : real,
      isar_compress_degree : int,
-     merge_timeout_slack : real,
      isar_try0 : bool,
      isar_minimize : bool,
      slice : bool,
@@ -351,7 +350,6 @@
    isar_proofs : bool option,
    isar_compress : real,
    isar_compress_degree : int,
-   merge_timeout_slack : real,
    isar_try0 : bool,
    isar_minimize : bool,
    slice : bool,
@@ -679,8 +677,8 @@
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     uncurried_aliases, fact_filter, max_facts, max_mono_iters,
                     max_new_mono_instances, isar_proofs, isar_compress,
-                    isar_compress_degree, merge_timeout_slack, isar_try0,
-                    isar_minimize, slice, timeout, preplay_timeout, ...})
+                    isar_compress_degree, isar_try0, isar_minimize, slice,
+                    timeout, preplay_timeout, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
@@ -956,9 +954,8 @@
                     ()
                 val isar_params =
                   (debug, verbose, preplay_timeout, isar_compress,
-                   isar_compress_degree, merge_timeout_slack, isar_try0,
-                   isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof,
-                   goal)
+                   isar_compress_degree, isar_try0, isar_minimize, pool,
+                   fact_names, lifted, sym_tab, atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command ctxt params minimize_command name
diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -12,7 +12,7 @@
   type one_line_params = Sledgehammer_Print.one_line_params
 
   type isar_params =
-    bool * bool * Time.time option * real * int * real * bool * bool
+    bool * bool * Time.time option * real * int * bool * bool
     * string Symtab.table * (string * stature) list vector
     * (string * term) list * int Symtab.table * string atp_proof * thm
 
@@ -408,14 +408,14 @@
   in chain_proof end
 
 type isar_params =
-  bool * bool * Time.time option * real * int * real * bool * bool
+  bool * bool * Time.time option * real * int * bool * bool
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string atp_proof * thm
 
 fun isar_proof_text ctxt isar_proofs
     (debug, verbose, preplay_timeout, isar_compress, isar_compress_degree,
-     merge_timeout_slack, isar_try0, isar_minimize, pool, fact_names, lifted,
-     sym_tab, atp_proof, goal)
+     isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof,
+     goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -592,7 +592,7 @@
           |> compress_proof
                (if isar_proofs = SOME true then isar_compress else 1000.0)
                (if isar_proofs = SOME true then isar_compress_degree else 100)
-               merge_timeout_slack preplay_interface
+               preplay_interface
           |> isar_try0 ? try0 preplay_timeout preplay_interface
           |> minimize_dependencies_and_remove_unrefed_steps isar_minimize
                preplay_interface