renamed Sledgehammer options
authorblanchet
Thu Jun 12 17:10:12 2014 +0200 (2014-06-12)
changeset 57245f6bf6d5341ee
parent 57244 ee08e7b8ad2b
child 57246 62746a41cc0c
renamed Sledgehammer options
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Metis_Examples/Sets.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:10:12 2014 +0200
     1.3 @@ -387,7 +387,7 @@
     1.4      SMT-LIB 2 and quantifiers.
     1.5  
     1.6  * Sledgehammer:
     1.7 -  - New prover "z3_new" with support for Isar proofs
     1.8 +  - "z3" can now produce Isar proofs
     1.9    - MaSh overhaul:
    1.10        - New SML-based learning engines eliminate the dependency on Python
    1.11          and increase performance and reliability.
    1.12 @@ -399,8 +399,8 @@
    1.13    - New option:
    1.14        smt_proofs
    1.15    - Renamed options:
    1.16 -      isar_compress ~> compress_isar
    1.17 -      isar_try0 ~> try0_isar
    1.18 +      isar_compress ~> compress
    1.19 +      isar_try0 ~> try0
    1.20      INCOMPATIBILITY.
    1.21  
    1.22  * Metis:
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:10:12 2014 +0200
     2.3 @@ -352,7 +352,7 @@
     2.4  \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
     2.5  that Isar proofs should be generated, in addition to one-line \textit{metis} or
     2.6  \textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
     2.7 -\textit{compress\_isar} (\S\ref{output-format}).
     2.8 +\textit{compress} (\S\ref{output-format}).
     2.9  
    2.10  \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
    2.11  provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
    2.12 @@ -1324,15 +1324,15 @@
    2.13  one-line proofs. If the option is set to \textit{smart} (the default), Isar
    2.14  proofs are only generated when no working one-line proof is available.
    2.15  
    2.16 -\opdefault{compress\_isar}{int}{\upshape 10}
    2.17 +\opdefault{compress}{int}{\upshape 10}
    2.18  Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
    2.19  is explicitly enabled. A value of $n$ indicates that each Isar proof step should
    2.20  correspond to a group of up to $n$ consecutive proof steps in the ATP proof.
    2.21  
    2.22 -\optrueonly{dont\_compress\_isar}
    2.23 -Alias for ``\textit{compress\_isar} = 0''.
    2.24 +\optrueonly{dont\_compress}
    2.25 +Alias for ``\textit{compress} = 0''.
    2.26  
    2.27 -\optrue{try0\_isar}{dont\_try0\_isar}
    2.28 +\optrue{try0}{dont\_try0}
    2.29  Specifies whether standard proof methods such as \textit{auto} and
    2.30  \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
    2.31  The collection of methods is roughly the same as for the \textbf{try0} command.
     3.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 12 17:02:03 2014 +0200
     3.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 12 17:10:12 2014 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  (*** Now various verions with an increasing shrink factor ***)
     3.6  
     3.7 -sledgehammer_params [isar_proofs, compress_isar = 1]
     3.8 +sledgehammer_params [isar_proofs, compress = 1]
     3.9  
    3.10  lemma
    3.11    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.12 @@ -60,7 +60,7 @@
    3.13    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
    3.14  qed
    3.15  
    3.16 -sledgehammer_params [isar_proofs, compress_isar = 2]
    3.17 +sledgehammer_params [isar_proofs, compress = 2]
    3.18  
    3.19  lemma
    3.20    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.21 @@ -83,7 +83,7 @@
    3.22    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
    3.23  qed
    3.24  
    3.25 -sledgehammer_params [isar_proofs, compress_isar = 3]
    3.26 +sledgehammer_params [isar_proofs, compress = 3]
    3.27  
    3.28  lemma
    3.29    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.30 @@ -103,7 +103,7 @@
    3.31    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
    3.32  qed
    3.33  
    3.34 -sledgehammer_params [isar_proofs, compress_isar = 4]
    3.35 +sledgehammer_params [isar_proofs, compress = 4]
    3.36  
    3.37  lemma
    3.38    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.39 @@ -123,7 +123,7 @@
    3.40    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
    3.41  qed
    3.42  
    3.43 -sledgehammer_params [isar_proofs, compress_isar = 1]
    3.44 +sledgehammer_params [isar_proofs, compress = 1]
    3.45  
    3.46  lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
    3.47  by (auto simp add: bigo_def bigo_pos_const)
     4.1 --- a/src/HOL/Metis_Examples/Sets.thy	Thu Jun 12 17:02:03 2014 +0200
     4.2 +++ b/src/HOL/Metis_Examples/Sets.thy	Thu Jun 12 17:10:12 2014 +0200
     4.3 @@ -21,7 +21,7 @@
     4.4  lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
     4.5  by metis
     4.6  
     4.7 -sledgehammer_params [isar_proofs, compress_isar = 1]
     4.8 +sledgehammer_params [isar_proofs, compress = 1]
     4.9  
    4.10  (*multiple versions of this example*)
    4.11  lemma (*equal_union: *)
    4.12 @@ -70,7 +70,7 @@
    4.13    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    4.14  qed
    4.15  
    4.16 -sledgehammer_params [isar_proofs, compress_isar = 2]
    4.17 +sledgehammer_params [isar_proofs, compress = 2]
    4.18  
    4.19  lemma (*equal_union: *)
    4.20     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    4.21 @@ -107,7 +107,7 @@
    4.22    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    4.23  qed
    4.24  
    4.25 -sledgehammer_params [isar_proofs, compress_isar = 3]
    4.26 +sledgehammer_params [isar_proofs, compress = 3]
    4.27  
    4.28  lemma (*equal_union: *)
    4.29     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    4.30 @@ -124,7 +124,7 @@
    4.31    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
    4.32  qed
    4.33  
    4.34 -sledgehammer_params [isar_proofs, compress_isar = 4]
    4.35 +sledgehammer_params [isar_proofs, compress = 4]
    4.36  
    4.37  lemma (*equal_union: *)
    4.38     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    4.39 @@ -140,7 +140,7 @@
    4.40    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
    4.41  qed
    4.42  
    4.43 -sledgehammer_params [isar_proofs, compress_isar = 1]
    4.44 +sledgehammer_params [isar_proofs, compress = 1]
    4.45  
    4.46  lemma (*equal_union: *)
    4.47     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
     5.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jun 12 17:02:03 2014 +0200
     5.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jun 12 17:10:12 2014 +0200
     5.3 @@ -44,7 +44,7 @@
     5.4  
     5.5  lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
     5.6         \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
     5.7 -(* sledgehammer [isar_proofs, compress_isar = 2] *)
     5.8 +(* sledgehammer [isar_proofs, compress = 2] *)
     5.9  proof -
    5.10    assume A1: "f c = Intg x"
    5.11    assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 17:02:03 2014 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 17:10:12 2014 +0200
     6.3 @@ -94,8 +94,8 @@
     6.4     ("max_mono_iters", "smart"),
     6.5     ("max_new_mono_instances", "smart"),
     6.6     ("isar_proofs", "smart"),
     6.7 -   ("compress_isar", "10"),
     6.8 -   ("try0_isar", "true"),
     6.9 +   ("compress", "10"),
    6.10 +   ("try0", "true"),
    6.11     ("smt_proofs", "smart"),
    6.12     ("slice", "true"),
    6.13     ("minimize", "smart"),
    6.14 @@ -104,7 +104,7 @@
    6.15  val alias_params =
    6.16    [("prover", ("provers", [])), (* undocumented *)
    6.17     ("dont_preplay", ("preplay_timeout", ["0"])),
    6.18 -   ("dont_compress_isar", ("compress_isar", ["0"])),
    6.19 +   ("dont_compress", ("compress", ["0"])),
    6.20     ("isar_proof", ("isar_proofs", [])) (* legacy *)]
    6.21  val negated_alias_params =
    6.22    [("no_debug", "debug"),
    6.23 @@ -118,7 +118,7 @@
    6.24     ("no_isar_proofs", "isar_proofs"),
    6.25     ("dont_slice", "slice"),
    6.26     ("dont_minimize", "minimize"),
    6.27 -   ("dont_try0_isar", "try0_isar"),
    6.28 +   ("dont_try0", "try0"),
    6.29     ("no_smt_proofs", "smt_proofs")]
    6.30  
    6.31  val params_not_for_minimize =
    6.32 @@ -299,8 +299,8 @@
    6.33      val max_new_mono_instances =
    6.34        lookup_option lookup_int "max_new_mono_instances"
    6.35      val isar_proofs = lookup_option lookup_bool "isar_proofs"
    6.36 -    val compress_isar = Real.max (1.0, lookup_real "compress_isar")
    6.37 -    val try0_isar = lookup_bool "try0_isar"
    6.38 +    val compress = Real.max (1.0, lookup_real "compress")
    6.39 +    val try0 = lookup_bool "try0"
    6.40      val smt_proofs = lookup_option lookup_bool "smt_proofs"
    6.41      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    6.42      val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    6.43 @@ -313,8 +313,8 @@
    6.44       uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
    6.45       max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    6.46       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    6.47 -     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
    6.48 -     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    6.49 +     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
    6.50 +     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    6.51    end
    6.52  
    6.53  fun get_params mode = extract_params mode o default_raw_params mode
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jun 12 17:02:03 2014 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jun 12 17:10:12 2014 +0200
     7.3 @@ -123,13 +123,13 @@
     7.4  
     7.5      fun isar_proof_of () =
     7.6        let
     7.7 -        val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
     7.8 -          atp_proof, goal) = isar_params ()
     7.9 +        val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
    7.10 +          isar_params ()
    7.11  
    7.12          val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
    7.13  
    7.14          fun massage_methods (meths as meth :: _) =
    7.15 -          if not try0_isar then [meth]
    7.16 +          if not try0 then [meth]
    7.17            else if smt_proofs = SOME true then SMT2_Method :: meths
    7.18            else meths
    7.19  
    7.20 @@ -138,7 +138,7 @@
    7.21          val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
    7.22  
    7.23          val do_preplay = preplay_timeout <> Time.zeroTime
    7.24 -        val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
    7.25 +        val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
    7.26  
    7.27          val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
    7.28          fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
    7.29 @@ -311,17 +311,17 @@
    7.30          val (play_outcome, isar_proof) =
    7.31            canonical_isar_proof
    7.32            |> tap (trace_isar_proof "Original")
    7.33 -          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
    7.34 +          |> compress_isar_proof ctxt compress preplay_timeout preplay_data
    7.35            |> tap (trace_isar_proof "Compressed")
    7.36            |> postprocess_isar_proof_remove_unreferenced_steps
    7.37                 (keep_fastest_method_of_isar_step (!preplay_data)
    7.38                  #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
    7.39            |> tap (trace_isar_proof "Minimized")
    7.40 -          (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
    7.41 +          (* It's not clear whether this is worth the trouble (and if so, "compress" has an
    7.42               unnatural semantics): *)
    7.43  (*
    7.44            |> minimize
    7.45 -               ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
    7.46 +               ? (compress_isar_proof ctxt compress preplay_timeout preplay_data
    7.47                    #> tap (trace_isar_proof "Compressed again"))
    7.48  *)
    7.49            |> `(preplay_outcome_of_isar_proof (!preplay_data))
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jun 12 17:02:03 2014 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jun 12 17:10:12 2014 +0200
     8.3 @@ -109,15 +109,15 @@
     8.4  val compress_degree = 2
     8.5  
     8.6  (* Precondition: The proof must be labeled canonically. *)
     8.7 -fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
     8.8 -  if compress_isar <= 1.0 then
     8.9 +fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof =
    8.10 +  if compress <= 1.0 then
    8.11      proof
    8.12    else
    8.13      let
    8.14        val (compress_further, decrement_step_count) =
    8.15          let
    8.16            val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
    8.17 -          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
    8.18 +          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress)
    8.19            val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
    8.20          in
    8.21            (fn () => !delta > 0, fn () => delta := !delta - 1)
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jun 12 17:02:03 2014 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jun 12 17:10:12 2014 +0200
     9.3 @@ -36,8 +36,8 @@
     9.4       max_mono_iters : int option,
     9.5       max_new_mono_instances : int option,
     9.6       isar_proofs : bool option,
     9.7 -     compress_isar : real,
     9.8 -     try0_isar : bool,
     9.9 +     compress : real,
    9.10 +     try0 : bool,
    9.11       smt_proofs : bool option,
    9.12       slice : bool,
    9.13       minimize : bool option,
    9.14 @@ -143,8 +143,8 @@
    9.15     max_mono_iters : int option,
    9.16     max_new_mono_instances : int option,
    9.17     isar_proofs : bool option,
    9.18 -   compress_isar : real,
    9.19 -   try0_isar : bool,
    9.20 +   compress : real,
    9.21 +   try0 : bool,
    9.22     smt_proofs : bool option,
    9.23     slice : bool,
    9.24     minimize : bool option,
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jun 12 17:02:03 2014 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jun 12 17:10:12 2014 +0200
    10.3 @@ -131,8 +131,8 @@
    10.4  
    10.5  fun run_atp mode name
    10.6      (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
    10.7 -       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
    10.8 -       try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
    10.9 +       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0,
   10.10 +       smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
   10.11      minimize_command
   10.12      ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   10.13    let
   10.14 @@ -371,8 +371,8 @@
   10.15                        |> introduce_spass_skolem
   10.16                        |> factify_atp_proof fact_names hyp_ts concl_t
   10.17                    in
   10.18 -                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
   10.19 -                     try0_isar, minimize <> SOME false, atp_proof, goal)
   10.20 +                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
   10.21 +                     minimize <> SOME false, atp_proof, goal)
   10.22                    end
   10.23                  val one_line_params =
   10.24                    (preplay, proof_banner mode name, used_facts,
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 17:02:03 2014 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 17:10:12 2014 +0200
    11.3 @@ -129,8 +129,8 @@
    11.4  fun print silent f = if silent then () else Output.urgent_message (f ())
    11.5  
    11.6  fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
    11.7 -      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
    11.8 -      smt_proofs, preplay_timeout, ...} : params)
    11.9 +      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
   11.10 +      preplay_timeout, ...} : params)
   11.11      silent (prover : prover) timeout i n state goal facts =
   11.12    let
   11.13      val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
   11.14 @@ -143,9 +143,9 @@
   11.15         uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
   11.16         max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
   11.17         max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
   11.18 -       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
   11.19 -       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
   11.20 -       preplay_timeout = preplay_timeout, expect = ""}
   11.21 +       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
   11.22 +       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
   11.23 +       expect = ""}
   11.24      val problem =
   11.25        {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
   11.26         factss = [("", facts)]}
   11.27 @@ -288,8 +288,8 @@
   11.28  fun adjust_proof_method_params override_params
   11.29      ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
   11.30        uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
   11.31 -      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
   11.32 -      timeout, preplay_timeout, expect} : params) =
   11.33 +      max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout,
   11.34 +      preplay_timeout, expect} : params) =
   11.35    let
   11.36      fun lookup_override name default_value =
   11.37        (case AList.lookup (op =) override_params name of
   11.38 @@ -304,8 +304,8 @@
   11.39       uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
   11.40       max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
   11.41       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
   11.42 -     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
   11.43 -     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   11.44 +     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
   11.45 +     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   11.46    end
   11.47  
   11.48  fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:02:03 2014 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:10:12 2014 +0200
    12.3 @@ -177,8 +177,8 @@
    12.4      do_slice timeout 1 NONE Time.zeroTime
    12.5    end
    12.6  
    12.7 -fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
    12.8 -      try0_isar, smt_proofs, minimize, preplay_timeout, ...})
    12.9 +fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
   12.10 +      minimize, preplay_timeout, ...})
   12.11      minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   12.12    let
   12.13      val thy = Proof.theory_of state
   12.14 @@ -201,8 +201,8 @@
   12.15           fn preplay =>
   12.16              let
   12.17                fun isar_params () =
   12.18 -                (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
   12.19 -                 minimize <> SOME false, atp_proof (), goal)
   12.20 +                (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize <> SOME false,
   12.21 +                 atp_proof (), goal)
   12.22  
   12.23                val one_line_params =
   12.24                  (preplay, proof_banner mode name, used_facts,