renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
authorblanchet
Mon Feb 03 19:32:02 2014 +0100 (2014-02-03)
changeset 552971dfcd49f5dcb
parent 55296 1d3dadda13a1
child 55298 53569ca831f4
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.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_smt.ML
     1.1 --- a/NEWS	Mon Feb 03 19:32:02 2014 +0100
     1.2 +++ b/NEWS	Mon Feb 03 19:32:02 2014 +0100
     1.3 @@ -116,7 +116,7 @@
     1.4  
     1.5  * Sledgehammer:
     1.6    - New option:
     1.7 -      smt
     1.8 +      smt_proofs
     1.9    - Renamed options:
    1.10        isar_compress ~> compress_isar
    1.11        isar_try0 ~> try0_isar
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 19:32:02 2014 +0100
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 19:32:02 2014 +0100
     2.3 @@ -117,7 +117,7 @@
     2.4  
     2.5  The result of a successful proof search is some source text that usually (but
     2.6  not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
     2.7 -proof relies on the general-purpose \textit{metis} proof method, which
     2.8 +proof typically relies on the general-purpose \textit{metis} proof method, which
     2.9  integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
    2.10  the kernel. Thus its results are correct by construction.
    2.11  
    2.12 @@ -296,7 +296,7 @@
    2.13  Waldmeister is run only for unit equational problems, where the goal's
    2.14  conclusion is a (universally quantified) equation.
    2.15  
    2.16 -For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
    2.17 +For each successful prover, Sledgehammer gives a one-line \textit{metis} or
    2.18  \textit{smt} method call. Rough timings are shown in parentheses, indicating how
    2.19  fast the call is. You can click the proof to insert it into the theory text.
    2.20  
    2.21 @@ -308,7 +308,7 @@
    2.22  \postw
    2.23  
    2.24  When Isar proof construction is successful, it can yield proofs that are more
    2.25 -readable and also faster than the \textit{metis} or \textit{smt} one-liners.
    2.26 +readable and also faster than the \textit{metis} or \textit{smt} one-line proofs.
    2.27  This feature is experimental and is only available for ATPs.
    2.28  
    2.29  \section{Hints}
    2.30 @@ -359,7 +359,7 @@
    2.31  if that helps.
    2.32  
    2.33  \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
    2.34 -that Isar proofs should be generated, in addition to one-liner \textit{metis} or
    2.35 +that Isar proofs should be generated, in addition to one-line \textit{metis} or
    2.36  \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
    2.37  \textit{compress\_isar} (\S\ref{output-format}).
    2.38  
    2.39 @@ -463,9 +463,8 @@
    2.40  
    2.41  \begin{enum}
    2.42  \item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
    2.43 -obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
    2.44 -Since the steps are fairly small, \textit{metis} is more likely to be able to
    2.45 -replay them.
    2.46 +obtain a step-by-step Isar proof. Since the steps are fairly small, \textit{metis}
    2.47 +and the other Isabelle proof methods are more likely to be able to replay them.
    2.48  
    2.49  \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
    2.50  It is usually stronger, but you need to either have Z3 available to replay the
    2.51 @@ -525,8 +524,8 @@
    2.52  versions of Metis. It is somewhat slower than \textit{metis}, but the proof
    2.53  search is fully typed, and it also includes more powerful rules such as the
    2.54  axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
    2.55 -higher-order places (e.g., in set comprehensions). The method kicks in
    2.56 -automatically as a fallback when \textit{metis} fails, and it is sometimes
    2.57 +higher-order places (e.g., in set comprehensions). The method is automatically
    2.58 +tried as a fallback when \textit{metis} fails, and it is sometimes
    2.59  generated by Sledgehammer instead of \textit{metis} if the proof obviously
    2.60  requires type information or if \textit{metis} failed when Sledgehammer
    2.61  preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
    2.62 @@ -1069,9 +1068,9 @@
    2.63  
    2.64  \opdefault{max\_facts}{smart\_int}{smart}
    2.65  Specifies the maximum number of facts that may be returned by the relevance
    2.66 -filter. If the option is set to \textit{smart}, it effectively takes a value
    2.67 -that was empirically found to be appropriate for the prover. Typical values
    2.68 -range between 50 and 1000.
    2.69 +filter. If the option is set to \textit{smart} (the default), it effectively
    2.70 +takes a value that was empirically found to be appropriate for the prover.
    2.71 +Typical values range between 50 and 1000.
    2.72  
    2.73  For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
    2.74  \textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
    2.75 @@ -1095,9 +1094,9 @@
    2.76  Specifies the maximum number of monomorphic instances to generate beyond
    2.77  \textit{max\_facts}. The higher this limit is, the more monomorphic instances
    2.78  are potentially generated. Whether monomorphization takes place depends on the
    2.79 -type encoding used. If the option is set to \textit{smart}, it takes a value
    2.80 -that was empirically found to be appropriate for the prover. For most provers,
    2.81 -this value is 100.
    2.82 +type encoding used. If the option is set to \textit{smart} (the default), it
    2.83 +takes a value that was empirically found to be appropriate for the prover. For
    2.84 +most provers, this value is 100.
    2.85  
    2.86  \nopagebreak
    2.87  {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
    2.88 @@ -1106,9 +1105,9 @@
    2.89  Specifies the maximum number of iterations for the monomorphization fixpoint
    2.90  construction. The higher this limit is, the more monomorphic instances are
    2.91  potentially generated. Whether monomorphization takes place depends on the
    2.92 -type encoding used. If the option is set to \textit{smart}, it takes a value
    2.93 -that was empirically found to be appropriate for the prover. For most provers,
    2.94 -this value is 3.
    2.95 +type encoding used. If the option is set to \textit{smart} (the default), it
    2.96 +takes a value that was empirically found to be appropriate for the prover.
    2.97 +For most provers, this value is 3.
    2.98  
    2.99  \nopagebreak
   2.100  {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
   2.101 @@ -1298,12 +1297,11 @@
   2.102  \textit{overlord} (\S\ref{mode-of-operation}).}
   2.103  
   2.104  \opsmart{isar\_proofs}{no\_isar\_proofs}
   2.105 -Specifies whether Isar proofs should be output in addition to one-liner
   2.106 -\textit{metis} proofs. The construction of Isar proof is still experimental and
   2.107 -may sometimes fail; however, when they succeed they are usually faster and more
   2.108 -intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
   2.109 -(the default), Isar proofs are only generated when no working one-liner
   2.110 -\textit{metis} proof is available.
   2.111 +Specifies whether Isar proofs should be output in addition to one-line proofs.
   2.112 +The construction of Isar proof is still experimental and may sometimes fail;
   2.113 +however, when they succeed they are usually faster and more intelligible than
   2.114 +one-line proofs. If the option is set to \textit{smart} (the default), Isar
   2.115 +proofs are only generated when no working one-line proof is available.
   2.116  
   2.117  \opdefault{compress\_isar}{int}{\upshape 10}
   2.118  Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
   2.119 @@ -1318,10 +1316,11 @@
   2.120  \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
   2.121  The collection of methods is roughly the same as for the \textbf{try0} command.
   2.122  
   2.123 -\opsmart{smt}{no\_smt}
   2.124 +\opsmart{smt\_proofs}{no\_smt\_proofs}
   2.125  Specifies whether the \textit{smt} proof method should be tried as an
   2.126 -alternative to \textit{metis}.  If the option is set to \textit{smart}, the
   2.127 -\textit{smt} method is used for one-line proofs but not in Isar proofs.
   2.128 +alternative to \textit{metis}.  If the option is set to \textit{smart} (the
   2.129 +default), the \textit{smt} method is used for one-line proofs but not in Isar
   2.130 +proofs.
   2.131  \end{enum}
   2.132  
   2.133  \subsection{Authentication}
   2.134 @@ -1357,10 +1356,10 @@
   2.135  searching for a proof. This excludes problem preparation and is a soft limit.
   2.136  
   2.137  \opdefault{preplay\_timeout}{float}{\upshape 2}
   2.138 -Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
   2.139 -should spend trying to ``preplay'' the found proof. If this option is set to 0,
   2.140 -no preplaying takes place, and no timing information is displayed next to the
   2.141 -suggested \textit{metis} calls.
   2.142 +Specifies the maximum number of seconds that \textit{metis} or other proof
   2.143 +methods should spend trying to ``preplay'' the found proof. If this option
   2.144 +is set to 0, no preplaying takes place, and no timing information is displayed
   2.145 +next to the suggested proof method calls.
   2.146  
   2.147  \nopagebreak
   2.148  {\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 19:32:02 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 19:32:02 2014 +0100
     3.3 @@ -96,7 +96,7 @@
     3.4     ("isar_proofs", "smart"),
     3.5     ("compress_isar", "10"),
     3.6     ("try0_isar", "true"),
     3.7 -   ("smt", "smart"),
     3.8 +   ("smt_proofs", "smart"),
     3.9     ("slice", "true"),
    3.10     ("minimize", "smart"),
    3.11     ("preplay_timeout", "2")]
    3.12 @@ -119,7 +119,7 @@
    3.13     ("dont_slice", "slice"),
    3.14     ("dont_minimize", "minimize"),
    3.15     ("dont_try0_isar", "try0_isar"),
    3.16 -   ("no_smt", "smt")]
    3.17 +   ("no_smt_proofs", "smt_proofs")]
    3.18  
    3.19  val params_not_for_minimize =
    3.20    ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
    3.21 @@ -288,7 +288,7 @@
    3.22      val isar_proofs = lookup_option lookup_bool "isar_proofs"
    3.23      val compress_isar = Real.max (1.0, lookup_real "compress_isar")
    3.24      val try0_isar = lookup_bool "try0_isar"
    3.25 -    val smt = lookup_option lookup_bool "smt"
    3.26 +    val smt_proofs = lookup_option lookup_bool "smt_proofs"
    3.27      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    3.28      val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    3.29      val timeout = lookup_time "timeout"
    3.30 @@ -300,7 +300,7 @@
    3.31       uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
    3.32       max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    3.33       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    3.34 -     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
    3.35 +     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
    3.36       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    3.37    end
    3.38  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
     4.3 @@ -126,7 +126,7 @@
     4.4  val skolem_methods =
     4.5    [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
     4.6  
     4.7 -fun isar_proof_text ctxt debug isar_proofs smt isar_params
     4.8 +fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     4.9      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    4.10    let
    4.11      fun isar_proof_of () =
    4.12 @@ -137,7 +137,9 @@
    4.13          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
    4.14  
    4.15          fun massage_meths (meths as meth :: _) =
    4.16 -          if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
    4.17 +          if not try0_isar then [meth]
    4.18 +          else if smt_proofs = SOME true then SMT_Method :: meths
    4.19 +          else meths
    4.20  
    4.21          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
    4.22          val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
    4.23 @@ -355,18 +357,18 @@
    4.24            if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
    4.25    in one_line_proof ^ isar_proof end
    4.26  
    4.27 -fun isar_proof_would_be_a_good_idea smt (meth, play) =
    4.28 +fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
    4.29    (case play of
    4.30 -    Played _ => meth = SMT_Method andalso smt <> SOME true
    4.31 +    Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
    4.32    | Play_Timed_Out _ => true
    4.33    | Play_Failed => true
    4.34    | Not_Played => false)
    4.35  
    4.36 -fun proof_text ctxt debug isar_proofs smt isar_params num_chained
    4.37 +fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
    4.38      (one_line_params as (preplay, _, _, _, _, _)) =
    4.39    (if isar_proofs = SOME true orelse
    4.40 -      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
    4.41 -     isar_proof_text ctxt debug isar_proofs smt isar_params
    4.42 +      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
    4.43 +     isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
    4.44     else
    4.45       one_line_proof_text num_chained) one_line_params
    4.46  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 19:32:02 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 19:32:02 2014 +0100
     5.3 @@ -38,7 +38,7 @@
     5.4       isar_proofs : bool option,
     5.5       compress_isar : real,
     5.6       try0_isar : bool,
     5.7 -     smt : bool option,
     5.8 +     smt_proofs : bool option,
     5.9       slice : bool,
    5.10       minimize : bool option,
    5.11       timeout : Time.time,
    5.12 @@ -147,7 +147,7 @@
    5.13     isar_proofs : bool option,
    5.14     compress_isar : real,
    5.15     try0_isar : bool,
    5.16 -   smt : bool option,
    5.17 +   smt_proofs : bool option,
    5.18     slice : bool,
    5.19     minimize : bool option,
    5.20     timeout : Time.time,
    5.21 @@ -183,7 +183,7 @@
    5.22    | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
    5.23    | _ => "Try this")
    5.24  
    5.25 -fun bunch_of_proof_methods smt needs_full_types desperate_lam_trans =
    5.26 +fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
    5.27    [Metis_Method (SOME full_type_enc, NONE)] @
    5.28    (if needs_full_types then
    5.29       [Metis_Method (SOME full_type_enc, NONE),
    5.30 @@ -193,7 +193,7 @@
    5.31       [Metis_Method (NONE, NONE),
    5.32        Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
    5.33    [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
    5.34 -  (if smt then [SMT_Method] else [])
    5.35 +  (if smt_proofs then [SMT_Method] else [])
    5.36  
    5.37  fun extract_proof_method ({type_enc, lam_trans, ...} : params)
    5.38        (Metis_Method (type_enc', lam_trans')) =
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:32:02 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:32:02 2014 +0100
     6.3 @@ -132,7 +132,7 @@
     6.4  fun run_atp mode name
     6.5      (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
     6.6         fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
     6.7 -       try0_isar, smt, slice, minimize, timeout, preplay_timeout, ...})
     6.8 +       try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
     6.9      minimize_command
    6.10      ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    6.11    let
    6.12 @@ -347,7 +347,7 @@
    6.13            val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
    6.14            val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
    6.15            val meths =
    6.16 -            bunch_of_proof_methods (smt <> SOME false) needs_full_types
    6.17 +            bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types
    6.18                (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
    6.19          in
    6.20            (used_facts,
    6.21 @@ -380,7 +380,7 @@
    6.22                     subgoal_count)
    6.23                  val num_chained = length (#facts (Proof.goal state))
    6.24                in
    6.25 -                proof_text ctxt debug isar_proofs smt isar_params num_chained one_line_params
    6.26 +                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
    6.27                end,
    6.28             (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
    6.29             (if important_message <> "" then
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
     7.3 @@ -129,8 +129,8 @@
     7.4  fun print silent f = if silent then () else Output.urgent_message (f ())
     7.5  
     7.6  fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
     7.7 -      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar, smt,
     7.8 -      preplay_timeout, ...} : params)
     7.9 +      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
    7.10 +      smt_proofs, preplay_timeout, ...} : params)
    7.11      silent (prover : prover) timeout i n state goal facts =
    7.12    let
    7.13      val _ =
    7.14 @@ -144,9 +144,9 @@
    7.15         uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
    7.16         max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
    7.17         max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
    7.18 -       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar, smt = smt,
    7.19 -       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
    7.20 -       expect = ""}
    7.21 +       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
    7.22 +       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
    7.23 +       preplay_timeout = preplay_timeout, expect = ""}
    7.24      val problem =
    7.25        {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
    7.26         factss = [("", facts)]}
    7.27 @@ -289,8 +289,8 @@
    7.28  fun adjust_proof_method_params override_params
    7.29      ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
    7.30        uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
    7.31 -      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt, slice, minimize, timeout,
    7.32 -      preplay_timeout, expect} : params) =
    7.33 +      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
    7.34 +      timeout, preplay_timeout, expect} : params) =
    7.35    let
    7.36      fun lookup_override name default_value =
    7.37        (case AList.lookup (op =) override_params name of
    7.38 @@ -305,7 +305,7 @@
    7.39       uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
    7.40       max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    7.41       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    7.42 -     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
    7.43 +     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
    7.44       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    7.45    end
    7.46  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 19:32:02 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 19:32:02 2014 +0100
     8.3 @@ -212,7 +212,7 @@
     8.4      do_slice timeout 1 NONE Time.zeroTime
     8.5    end
     8.6  
     8.7 -fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
     8.8 +fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
     8.9      minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    8.10    let
    8.11      val thy = Proof.theory_of state
    8.12 @@ -234,7 +234,7 @@
    8.13          NONE =>
    8.14          (Lazy.lazy (fn () =>
    8.15             play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
    8.16 -             SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
    8.17 +             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
    8.18           fn preplay =>
    8.19              let
    8.20                val one_line_params =