# HG changeset patch
# User blanchet
# Date 1402585812 -7200
# Node ID f6bf6d5341ee443b2eac32309e97e3fda0464f89
# Parent  ee08e7b8ad2b1b84662c553a4511bfc31263d48b
renamed Sledgehammer options

diff -r ee08e7b8ad2b -r f6bf6d5341ee NEWS
--- a/NEWS	Thu Jun 12 17:02:03 2014 +0200
+++ b/NEWS	Thu Jun 12 17:10:12 2014 +0200
@@ -387,7 +387,7 @@
     SMT-LIB 2 and quantifiers.
 
 * Sledgehammer:
-  - New prover "z3_new" with support for Isar proofs
+  - "z3" can now produce Isar proofs
   - MaSh overhaul:
       - New SML-based learning engines eliminate the dependency on Python
         and increase performance and reliability.
@@ -399,8 +399,8 @@
   - New option:
       smt_proofs
   - Renamed options:
-      isar_compress ~> compress_isar
-      isar_try0 ~> try0_isar
+      isar_compress ~> compress
+      isar_try0 ~> try0
     INCOMPATIBILITY.
 
 * Metis:
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:10:12 2014 +0200
@@ -352,7 +352,7 @@
 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
 that Isar proofs should be generated, in addition to one-line \textit{metis} or
 \textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
-\textit{compress\_isar} (\S\ref{output-format}).
+\textit{compress} (\S\ref{output-format}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
@@ -1324,15 +1324,15 @@
 one-line proofs. If the option is set to \textit{smart} (the default), Isar
 proofs are only generated when no working one-line proof is available.
 
-\opdefault{compress\_isar}{int}{\upshape 10}
+\opdefault{compress}{int}{\upshape 10}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
 is explicitly enabled. A value of $n$ indicates that each Isar proof step should
 correspond to a group of up to $n$ consecutive proof steps in the ATP proof.
 
-\optrueonly{dont\_compress\_isar}
-Alias for ``\textit{compress\_isar} = 0''.
+\optrueonly{dont\_compress}
+Alias for ``\textit{compress} = 0''.
 
-\optrue{try0\_isar}{dont\_try0\_isar}
+\optrue{try0}{dont\_try0}
 Specifies whether standard proof methods such as \textit{auto} and
 \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
 The collection of methods is roughly the same as for the \textbf{try0} command.
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 12 17:10:12 2014 +0200
@@ -29,7 +29,7 @@
 
 (*** Now various verions with an increasing shrink factor ***)
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 2]
+sledgehammer_params [isar_proofs, compress = 2]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 3]
+sledgehammer_params [isar_proofs, compress = 3]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 4]
+sledgehammer_params [isar_proofs, compress = 4]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Metis_Examples/Sets.thy
--- a/src/HOL/Metis_Examples/Sets.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Metis_Examples/Sets.thy	Thu Jun 12 17:10:12 2014 +0200
@@ -21,7 +21,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -70,7 +70,7 @@
   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
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 2]
+sledgehammer_params [isar_proofs, compress = 2]
 
 lemma (*equal_union: *)
    "(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))"
@@ -107,7 +107,7 @@
   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
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 3]
+sledgehammer_params [isar_proofs, compress = 3]
 
 lemma (*equal_union: *)
    "(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))"
@@ -124,7 +124,7 @@
   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)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 4]
+sledgehammer_params [isar_proofs, compress = 4]
 
 lemma (*equal_union: *)
    "(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))"
@@ -140,7 +140,7 @@
   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)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 lemma (*equal_union: *)
    "(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))"
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Metis_Examples/Trans_Closure.thy
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jun 12 17:10:12 2014 +0200
@@ -44,7 +44,7 @@
 
 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>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proofs, compress_isar = 2] *)
+(* sledgehammer [isar_proofs, compress = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -94,8 +94,8 @@
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "smart"),
-   ("compress_isar", "10"),
-   ("try0_isar", "true"),
+   ("compress", "10"),
+   ("try0", "true"),
    ("smt_proofs", "smart"),
    ("slice", "true"),
    ("minimize", "smart"),
@@ -104,7 +104,7 @@
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
-   ("dont_compress_isar", ("compress_isar", ["0"])),
+   ("dont_compress", ("compress", ["0"])),
    ("isar_proof", ("isar_proofs", [])) (* legacy *)]
 val negated_alias_params =
   [("no_debug", "debug"),
@@ -118,7 +118,7 @@
    ("no_isar_proofs", "isar_proofs"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
-   ("dont_try0_isar", "try0_isar"),
+   ("dont_try0", "try0"),
    ("no_smt_proofs", "smt_proofs")]
 
 val params_not_for_minimize =
@@ -299,8 +299,8 @@
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
-    val compress_isar = Real.max (1.0, lookup_real "compress_isar")
-    val try0_isar = lookup_bool "try0_isar"
+    val compress = Real.max (1.0, lookup_real "compress")
+    val try0 = lookup_bool "try0"
     val smt_proofs = lookup_option lookup_bool "smt_proofs"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -313,8 +313,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params mode
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -123,13 +123,13 @@
 
     fun isar_proof_of () =
       let
-        val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
-          atp_proof, goal) = isar_params ()
+        val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
+          isar_params ()
 
         val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
 
         fun massage_methods (meths as meth :: _) =
-          if not try0_isar then [meth]
+          if not try0 then [meth]
           else if smt_proofs = SOME true then SMT2_Method :: meths
           else meths
 
@@ -138,7 +138,7 @@
         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
 
         val do_preplay = preplay_timeout <> Time.zeroTime
-        val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
+        val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
 
         val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
         fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
@@ -311,17 +311,17 @@
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
-          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
+          |> compress_isar_proof ctxt compress preplay_timeout preplay_data
           |> tap (trace_isar_proof "Compressed")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
-          (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
+          (* It's not clear whether this is worth the trouble (and if so, "compress" has an
              unnatural semantics): *)
 (*
           |> minimize
-               ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
+               ? (compress_isar_proof ctxt compress preplay_timeout preplay_data
                   #> tap (trace_isar_proof "Compressed again"))
 *)
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -109,15 +109,15 @@
 val compress_degree = 2
 
 (* Precondition: The proof must be labeled canonically. *)
-fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
-  if compress_isar <= 1.0 then
+fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof =
+  if compress <= 1.0 then
     proof
   else
     let
       val (compress_further, decrement_step_count) =
         let
           val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
-          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
+          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress)
           val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
         in
           (fn () => !delta > 0, fn () => delta := !delta - 1)
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -36,8 +36,8 @@
      max_mono_iters : int option,
      max_new_mono_instances : int option,
      isar_proofs : bool option,
-     compress_isar : real,
-     try0_isar : bool,
+     compress : real,
+     try0 : bool,
      smt_proofs : bool option,
      slice : bool,
      minimize : bool option,
@@ -143,8 +143,8 @@
    max_mono_iters : int option,
    max_new_mono_instances : int option,
    isar_proofs : bool option,
-   compress_isar : real,
-   try0_isar : bool,
+   compress : real,
+   try0 : bool,
    smt_proofs : bool option,
    slice : bool,
    minimize : bool option,
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -131,8 +131,8 @@
 
 fun run_atp mode name
     (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, compress_isar,
-       try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
+       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0,
+       smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
     minimize_command
     ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
@@ -371,8 +371,8 @@
                       |> introduce_spass_skolem
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
-                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
-                     try0_isar, minimize <> SOME false, atp_proof, goal)
+                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
+                     minimize <> SOME false, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -129,8 +129,8 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
-      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
-      smt_proofs, preplay_timeout, ...} : params)
+      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
+      preplay_timeout, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -143,9 +143,9 @@
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
        max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
        max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
-       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
-       preplay_timeout = preplay_timeout, expect = ""}
+       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
+       expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
@@ -288,8 +288,8 @@
 fun adjust_proof_method_params override_params
     ({debug, verbose, overlord, spy, 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, compress_isar, try0_isar, smt_proofs, slice, minimize,
-      timeout, preplay_timeout, expect} : params) =
+      max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout,
+      preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       (case AList.lookup (op =) override_params name of
@@ -304,8 +304,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
diff -r ee08e7b8ad2b -r f6bf6d5341ee src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -177,8 +177,8 @@
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
-      try0_isar, smt_proofs, minimize, preplay_timeout, ...})
+fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
+      minimize, preplay_timeout, ...})
     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -201,8 +201,8 @@
          fn preplay =>
             let
               fun isar_params () =
-                (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
-                 minimize <> SOME false, atp_proof (), goal)
+                (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize <> SOME false,
+                 atp_proof (), goal)
 
               val one_line_params =
                 (preplay, proof_banner mode name, used_facts,