merged
authorhaftmann
Tue, 09 Aug 2011 18:52:18 +0200
changeset 44105 04e51b7a3422
parent 44102 954e9d6782ea (diff)
parent 44104 50c067b51135 (current diff)
child 44106 0e018cbcc0de
merged
--- a/doc-src/IsarRef/Thy/Generic.thy	Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Tue Aug 09 18:52:18 2011 +0200
@@ -201,7 +201,7 @@
   @{rail "
     @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     ;
-    @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
+    @@{method split} @{syntax thmrefs}
   "}
 
   These methods provide low-level facilities for equational reasoning
@@ -245,12 +245,13 @@
   t"} where @{text x} is a free or bound variable.
 
   \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
-  splitting using the given rules.  By default, splitting is performed
-  in the conclusion of a goal; the @{text "(asm)"} option indicates to
-  operate on assumptions instead.
+  splitting using the given rules.  Splitting is performed in the
+  conclusion or some assumption of the subgoal, depending of the
+  structure of the rule.
   
   Note that the @{method simp} method already involves repeated
-  application of split rules as declared in the current context.
+  application of split rules as declared in the current context, using
+  @{attribute split}, for example.
 
   \end{description}
 *}
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue Aug 09 18:52:18 2011 +0200
@@ -336,14 +336,8 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
 \rail@end
-\rail@begin{2}{}
+\rail@begin{1}{}
 \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{asm}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
 \rail@end
 \end{railoutput}
@@ -388,12 +382,13 @@
   assumption; this only works for equations of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} where \isa{x} is a free or bound variable.
 
   \item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs single-step case
-  splitting using the given rules.  By default, splitting is performed
-  in the conclusion of a goal; the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option indicates to
-  operate on assumptions instead.
+  splitting using the given rules.  Splitting is performed in the
+  conclusion or some assumption of the subgoal, depending of the
+  structure of the rule.
   
   Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
-  application of split rules as declared in the current context.
+  application of split rules as declared in the current context, using
+  \hyperlink{attribute.split}{\mbox{\isa{split}}}, for example.
 
   \end{description}%
 \end{isamarkuptext}%
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 09 18:52:18 2011 +0200
@@ -85,15 +85,14 @@
 
 Sledgehammer is a tool that applies automatic theorem provers (ATPs)
 and satisfiability-modulo-theories (SMT) solvers on the current goal. The
-supported ATPs are E \cite{schulz-2002}, LEO-II \cite{leo2}, Satallax
-\cite{satallax}, SInE-E \cite{sine}, SNARK \cite{snark}, SPASS
-\cite{weidenbach-et-al-2009}, ToFoF-E \cite{tofof}, Vampire
-\cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
-run either locally or remotely via the System\-On\-TPTP web service
-\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
-used by default, and you can tell Sledgehammer to try CVC3 \cite{cvc3} and Yices
-\cite{yices} as well; these are run either locally or on a server at the TU
-M\"unchen.
+supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF
+\cite{tofof}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark},
+SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
+Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
+the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
+the SMT solvers Z3 \cite{z3} is used by default, and you can tell Sledgehammer
+to try CVC3 \cite{cvc3} and Yices \cite{yices} as well; these are run either
+locally or on a server at the TU M\"unchen.
 
 The problem passed to the automatic provers consists of your current goal
 together with a heuristic selection of hundreds of facts (theorems) from the
@@ -141,10 +140,10 @@
 
 \subsection{Installing ATPs}
 
-Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
-LEO-II, Satallax, SInE-E, SNARK, ToFoF-E, and Waldmeister are available remotely
-via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
-should at least install E and SPASS locally.
+Currently, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
+addition, E, E-SInE, E-ToFoF, LEO-II, Satallax, SNARK, Waldmeister, and Vampire
+are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want
+better performance, you should at least install E and SPASS locally.
 
 There are three main ways to install ATPs on your machine:
 
@@ -266,7 +265,7 @@
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\
+Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
 %
@@ -275,7 +274,7 @@
 Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
 \postw
 
-Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
 Depending on which provers are installed and how many processor cores are
 available, some of the provers might be missing or present with a
 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
@@ -525,7 +524,7 @@
 it took to find it or replay it).
 
 In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
-proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
+proofs or sometimes produce incomplete proofs. The minimizer is then invoked to
 find out which facts are actually needed from the (large) set of facts that was
 initinally given to the prover. Finally, if a prover returns a proof with lots
 of facts, the minimizer is invoked automatically since Metis would be unlikely
@@ -723,6 +722,23 @@
 executable, or install the prebuilt E package from Isabelle's download page. See
 \S\ref{installation} for details.
 
+\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
+higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
+with support for the TPTP higher-order syntax (THF).
+
+\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
+the external provers, Metis itself can be used for proof search.
+
+\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
+Metis, corresponding to \textit{metis} (\textit{full\_types}).
+
+\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
+corresponding to \textit{metis} (\textit{no\_types}).
+
+\item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
+higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
+support for the TPTP higher-order syntax (THF).
+
 \item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
@@ -730,17 +746,17 @@
 package from Isabelle's download page. Sledgehammer requires version 3.5 or
 above. See \S\ref{installation} for details.
 
-\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
-SRI \cite{yices}. To use Yices, set the environment variable
-\texttt{YICES\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version 1.0.
-
 \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is a first-order resolution
 prover developed by Andrei Voronkov and his colleagues
 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
 executable. Sledgehammer has been tested with versions 11, 0.6, and 1.0.
 
+\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
+SRI \cite{yices}. To use Yices, set the environment variable
+\texttt{YICES\_SOLVER} to the complete path of the executable, including the
+file name. Sledgehammer has been tested with version 1.0.
+
 \item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable
 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
@@ -750,15 +766,6 @@
 \item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
 ATP, exploiting Z3's undocumented support for the TPTP format. It is included
 for experimental purposes. It requires version 2.18 or above.
-
-\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
-the external provers, Metis itself can be used for proof search.
-
-\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
-Metis, corresponding to \textit{metis} (\textit{full\_types}).
-
-\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
-corresponding to \textit{metis} (\textit{no\_types}).
 \end{enum}
 
 In addition, the following remote provers are supported:
@@ -771,32 +778,26 @@
 \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic
-higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP higher-order syntax (THF). The remote version of
-LEO-II runs on Geoff Sutcliffe's Miami servers. In the current setup, the
-problems given to LEO-II are only mildly higher-order.
-
-\item[$\bullet$] \textbf{\textit{remote\_satallax}:} Satallax is an automatic
-higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
-support for the TPTP higher-order syntax (THF). The remote version of Satallax
-runs on Geoff Sutcliffe's Miami servers. In the current setup, the problems
-given to Satallax are only mildly higher-order.
-
-\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
+\item[$\bullet$] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
 SInE runs on Geoff Sutcliffe's Miami servers.
 
+\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
+developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
+servers. This ATP supports the TPTP many-typed first-order format (TFF). The
+remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
+
+\item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
+runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
+\item[$\bullet$] \textbf{\textit{remote\_satallax}:} The remote version of
+Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
 \item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
 resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
 TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
 Geoff Sutcliffe's Miami servers.
 
-\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
-developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP many-typed first-order format (TFF). The
-remote version of ToFoF-E runs on Geoff Sutcliffe's Miami servers.
-
 \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
 Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
 
@@ -814,12 +815,12 @@
 as an ATP'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
-By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
-the SMT module's \textit{smt\_solver} configuration option is set to) in
-parallel---either locally or remotely, depending on the number of processor
-cores available. For historical reasons, the default value of this option can be
-overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
-in Proof General.
+By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
+the SMT module's \textit{smt\_solver} configuration option is set to), and (if
+appropriate) Waldmeister in parallel---either locally or remotely, depending on
+the number of processor cores available. For historical reasons, the default
+value of this option can be overridden using the option ``Sledgehammer:
+Provers'' from the ``Isabelle'' menu in Proof General.
 
 It is a good idea to run several provers in parallel, although it could slow
 down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
--- a/doc-src/manual.bib	Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/manual.bib	Tue Aug 09 18:52:18 2011 +0200
@@ -140,7 +140,7 @@
 
 %B
 
-@inproceedings{satallax,
+@inproceedings{backes-brown-2010,
   title = "Analytic Tableaux for Higher-Order Logic with Choice",
   author = "Julian Backes and Chad E. Brown",
   booktitle={Automated Reasoning: IJCAR 2010},
@@ -335,6 +335,17 @@
   publisher	= {Academic Press},
   year		= 1988}
 
+@inproceedings{satallax,
+  author = "Chad E. Brown",
+  title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems",
+  booktitle = {Automated Deduction --- CADE-23},
+  publisher = Springer,
+  series = LNCS,
+  volume = 6803,
+  pages = "147--161",
+  editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+  year = 2011}
+
 @Article{debruijn72,
   author	= {N. G. de Bruijn},
   title		= {Lambda Calculus Notation with Nameless Dummies,
@@ -686,9 +697,10 @@
   booktitle = {Automated Deduction --- CADE-23},
   publisher = Springer,
   series = LNCS,
+  volume = 6803,
+  pages = "299--314",
   editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
-  year = 2011,
-  note = "To appear."}
+  year = 2011}
 
 @book{Hudak-Haskell,author={Paul Hudak},
 title={The Haskell School of Expression},publisher=CUP,year=2000}
--- a/src/HOL/ATP.thy	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/ATP.thy	Tue Aug 09 18:52:18 2011 +0200
@@ -7,7 +7,8 @@
 
 theory ATP
 imports Meson
-uses "Tools/monomorph.ML"
+uses "Tools/lambda_lifting.ML"
+     "Tools/monomorph.ML"
      "Tools/ATP/atp_util.ML"
      "Tools/ATP/atp_problem.ML"
      "Tools/ATP/atp_proof.ML"
--- a/src/HOL/IsaMakefile	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 09 18:52:18 2011 +0200
@@ -244,7 +244,9 @@
   Tools/inductive_codegen.ML \
   Tools/inductive_realizer.ML \
   Tools/inductive_set.ML \
+  Tools/lambda_lifting.ML \
   Tools/lin_arith.ML \
+  Tools/monomorph.ML \
   Tools/nat_arith.ML \
   Tools/primrec.ML \
   Tools/prop_logic.ML \
@@ -309,10 +311,8 @@
   Tools/code_evaluation.ML \
   Tools/groebner.ML \
   Tools/int_arith.ML \
-  Tools/lambda_lifting.ML \
   Tools/list_code.ML \
   Tools/list_to_set_comprehension.ML \
-  Tools/monomorph.ML \
   Tools/nat_numeral_simprocs.ML \
   Tools/Nitpick/kodkod.ML \
   Tools/Nitpick/kodkod_sat.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -9,11 +9,11 @@
 val prover_timeoutK = "prover_timeout"
 val keepK = "keep"
 val type_encK = "type_enc"
+val soundK = "sound"
 val slicingK = "slicing"
 val lambda_translationK = "lambda_translation"
 val e_weight_methodK = "e_weight_method"
-val spass_force_sosK = "spass_force_sos"
-val vampire_force_sosK = "vampire_force_sos"
+val force_sosK = "force_sos"
 val max_relevantK = "max_relevant"
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
@@ -213,6 +213,8 @@
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
 
+val str0 = string_of_int o the_default 0
+
 local
 
 val str = string_of_int
@@ -242,13 +244,9 @@
     str3 (avg_time time_prover_fail (calls - success)))
   )
 
-
 fun str_of_pos (pos, triv) =
-  let val str0 = string_of_int o the_default 0
-  in
-    str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
-    (if triv then "[T]" else "")
-  end
+  str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
+  (if triv then "[T]" else "")
 
 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
      re_nontriv_success, re_proofs, re_time, re_timeout,
@@ -354,35 +352,36 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
-      e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
-      st =
+fun run_sh prover_name prover type_enc sound max_relevant slicing
+        lambda_translation e_weight_method force_sos hard_timeout timeout dir
+        pos st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
-    fun change_dir (SOME dir) =
+    fun set_file_name (SOME dir) =
         Config.put Sledgehammer_Provers.dest_dir dir
+        #> Config.put Sledgehammer_Provers.problem_prefix
+          ("prob_" ^ str0 (Position.line_of pos))
         #> Config.put SMT_Config.debug_files
           (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
           ^ serial_string ())
-      | change_dir NONE = I
+      | set_file_name NONE = I
     val st' =
       st |> Proof.map_context
-                (change_dir dir
+                (set_file_name dir
                  #> (Option.map (Config.put
                        Sledgehammer_Provers.atp_lambda_translation)
                        lambda_translation |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.e_weight_method)
                        e_weight_method |> the_default I)
-                 #> (Option.map (Config.put ATP_Systems.spass_force_sos)
-                       spass_force_sos |> the_default I)
-                 #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
-                       vampire_force_sos |> the_default I)
+                 #> (Option.map (Config.put ATP_Systems.force_sos)
+                       force_sos |> the_default I)
                  #> Config.put Sledgehammer_Provers.measure_run_time true)
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_enc", type_enc),
+           ("sound", sound),
            ("max_relevant", max_relevant),
            ("slicing", slicing),
            ("timeout", string_of_int timeout)]
@@ -451,20 +450,20 @@
 
 in
 
-fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_sledgehammer trivial args reconstructor named_thms id
+      ({pre=st, log, pos, ...}: Mirabelle.run_args) =
   let
     val triv_str = if trivial then "[T] " else ""
     val _ = change_data id inc_sh_calls
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_prover (Proof.context_of st) args
     val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+    val sound = AList.lookup (op =) args soundK |> the_default "false"
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val slicing = AList.lookup (op =) args slicingK |> the_default "true"
     val lambda_translation = AList.lookup (op =) args lambda_translationK
     val e_weight_method = AList.lookup (op =) args e_weight_methodK
-    val spass_force_sos = AList.lookup (op =) args spass_force_sosK
-      |> Option.map (curry (op <>) "false")
-    val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
+    val force_sos = AList.lookup (op =) args force_sosK
       |> Option.map (curry (op <>) "false")
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
@@ -472,9 +471,9 @@
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_enc max_relevant slicing lambda_translation
-        e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
-        dir st
+      run_sh prover_name prover type_enc sound max_relevant slicing
+        lambda_translation e_weight_method force_sos hard_timeout timeout dir
+        pos st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
@@ -511,6 +510,7 @@
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_prover ctxt args
     val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+    val sound = AList.lookup (op =) args soundK |> the_default "false"
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
@@ -519,6 +519,7 @@
       [("provers", prover_name),
        ("verbose", "true"),
        ("type_enc", type_enc),
+       ("sound", sound),
        ("timeout", string_of_int timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts prover_name params
--- a/src/HOL/SMT.thy	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/SMT.thy	Tue Aug 09 18:52:18 2011 +0200
@@ -7,7 +7,6 @@
 theory SMT
 imports Record
 uses
-  "Tools/lambda_lifting.ML"
   "Tools/SMT/smt_utils.ML"
   "Tools/SMT/smt_failure.ML"
   "Tools/SMT/smt_config.ML"
--- a/src/HOL/TPTP/atp_export.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -160,8 +160,7 @@
       facts
       |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
       |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
-                             (rpair [] o map (introduce_combinators ctxt))
-                             false true [] @{prop False}
+                             combinatorsN false true [] @{prop False}
     val atp_problem =
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -25,6 +25,7 @@
      best_slices :
        Proof.context -> (real * (bool * (int * string * string))) list}
 
+  val force_sos : bool Config.T
   val e_smartN : string
   val e_autoN : string
   val e_fun_weightN : string
@@ -36,16 +37,14 @@
   val e_default_sym_offs_weight : real Config.T
   val e_sym_offs_weight_base : real Config.T
   val e_sym_offs_weight_span : real Config.T
-  val spass_force_sos : bool Config.T
-  val vampire_force_sos : bool Config.T
   val eN : string
   val spassN : string
   val vampireN : string
   val leo2N : string
   val satallaxN : string
-  val sine_eN : string
+  val e_sineN : string
   val snarkN : string
-  val tofof_eN : string
+  val e_tofofN : string
   val waldmeisterN : string
   val z3_atpN : string
   val remote_prefix : string
@@ -103,14 +102,14 @@
 (* named ATPs *)
 
 val eN = "e"
+val leo2N = "leo2"
+val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
 val z3_atpN = "z3_atp"
-val leo2N = "leo2"
-val satallaxN = "satallax"
-val sine_eN = "sine_e"
+val e_sineN = "e_sine"
 val snarkN = "snark"
-val tofof_eN = "tofof_e"
+val e_tofofN = "e_tofof"
 val waldmeisterN = "waldmeister"
 val remote_prefix = "remote_"
 
@@ -128,6 +127,8 @@
 val sosN = "sos"
 val no_sosN = "no_sos"
 
+val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
+
 
 (* E *)
 
@@ -228,10 +229,49 @@
 val e = (eN, e_config)
 
 
-(* SPASS *)
+(* LEO-II *)
+
+val leo2_config : atp_config =
+  {exec = ("LEO2_HOME", "leo"),
+   required_execs = [],
+   arguments =
+     fn _ => fn _ => fn sos => fn timeout => fn _ =>
+        "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
+        |> sos = sosN ? prefix "--sos ",
+   proof_delims = tstp_proof_delims,
+   known_failures = [],
+   conj_sym_kind = Axiom,
+   prem_kind = Hypothesis,
+   formats = [THF, FOF],
+   best_slices = fn ctxt =>
+     (* FUDGE *)
+     [(0.667, (false, (150, "simple_higher", sosN))),
+      (0.333, (true, (50, "simple_higher", no_sosN)))]
+     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+         else I)}
 
-val spass_force_sos =
-  Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
+val leo2 = (leo2N, leo2_config)
+
+
+(* Satallax *)
+
+val satallax_config : atp_config =
+  {exec = ("SATALLAX_HOME", "satallax"),
+   required_execs = [],
+   arguments =
+     fn _ => fn _ => fn _ => fn timeout => fn _ =>
+        "-t " ^ string_of_int (to_secs 1 timeout),
+   proof_delims = tstp_proof_delims,
+   known_failures = [(ProofMissing, "SZS status Theorem")],
+   conj_sym_kind = Axiom,
+   prem_kind = Hypothesis,
+   formats = [THF],
+   best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+
+val satallax = (satallaxN, satallax_config)
+
+
+(* SPASS *)
 
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of "hAPP". *)
@@ -260,7 +300,7 @@
      [(0.333, (false, (150, "mangled_tags", sosN))),
       (0.333, (false, (300, "poly_tags?", sosN))),
       (0.334, (true, (50, "mangled_tags?", no_sosN)))]
-     |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
+     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val spass = (spassN, spass_config)
@@ -268,9 +308,6 @@
 
 (* Vampire *)
 
-val vampire_force_sos =
-  Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
-
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
@@ -301,7 +338,7 @@
      [(0.333, (false, (150, "poly_guards", sosN))),
       (0.334, (true, (50, "mangled_guards?", no_sosN))),
       (0.333, (false, (500, "mangled_tags?", sosN)))]
-     |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
+     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val vampire = (vampireN, vampire_config)
@@ -411,26 +448,26 @@
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
                (K (750, "mangled_tags?") (* FUDGE *))
+val remote_leo2 =
+  remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
+               (K (100, "simple_higher") (* FUDGE *))
+val remote_satallax =
+  remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
+               (K (100, "simple_higher") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
                (K (200, "mangled_guards?") (* FUDGE *))
 val remote_z3_atp =
   remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
-val remote_leo2 =
-  remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
-             (K (100, "simple_higher") (* FUDGE *))
-val remote_satallax =
-  remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
-             (K (64, "simple_higher") (* FUDGE *))
-val remote_sine_e =
-  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
+val remote_e_sine =
+  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
              [TFF, FOF] (K (100, "simple") (* FUDGE *))
-val remote_tofof_e =
-  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
+val remote_e_tofof =
+  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
              Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
@@ -461,9 +498,9 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
-   remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
-   remote_waldmeister]
+  [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
+   remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+   remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps
 
 end;
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -31,6 +31,13 @@
     Guards of polymorphism * type_level * type_heaviness |
     Tags of polymorphism * type_level * type_heaviness
 
+  val no_lambdasN : string
+  val concealedN : string
+  val liftingN : string
+  val combinatorsN : string
+  val hybridN : string
+  val lambdasN : string
+  val smartN : string
   val bound_var_prefix : string
   val schematic_var_prefix : string
   val fixed_var_prefix : string
@@ -88,11 +95,10 @@
   val unmangled_const_name : string -> string
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
-  val introduce_combinators : Proof.context -> term -> term
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
-    -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
-    -> term -> ((string * locality) * term) list
+    -> bool -> string -> bool -> bool -> term list -> term
+    -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
        * (string * locality) list vector * int list * int Symtab.table
   val atp_problem_weights : string problem -> (string * real) list
@@ -106,6 +112,14 @@
 
 type name = string * string
 
+val no_lambdasN = "no_lambdas"
+val concealedN = "concealed"
+val liftingN = "lifting"
+val combinatorsN = "combinators"
+val hybridN = "hybrid"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
 val generate_info = false (* experimental *)
 
 fun isabelle_info s =
@@ -606,6 +620,29 @@
                  | _ => type_enc)
      | format => (format, type_enc))
 
+fun lift_lambdas ctxt type_enc =
+  map (close_form o Envir.eta_contract) #> rpair ctxt
+  #-> Lambda_Lifting.lift_lambdas
+          (if polymorphism_of_type_enc type_enc = Polymorphic then
+             SOME polymorphic_free_prefix
+           else
+             NONE)
+          Lambda_Lifting.is_quantifier
+  #> fst
+
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
+    intentionalize_def t
+  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+    let
+      fun lam T t = Abs (Name.uu, T, t)
+      val (head, args) = strip_comb t ||> rev
+      val head_T = fastype_of head
+      val n = length args
+      val arg_Ts = head_T |> binder_types |> take n |> rev
+      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
+  | intentionalize_def t = t
+
 type translated_formula =
   {name : string,
    locality : locality,
@@ -834,8 +871,13 @@
              | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
              | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
              | (false, s) =>
-               if is_tptp_equal s then IConst (`I tptp_equal, T, [])
-               else IConst (proxy_base |>> prefix const_prefix, T, T_args)
+               if is_tptp_equal s andalso length args = 2 then
+                 IConst (`I tptp_equal, T, [])
+               else
+                 (* Use a proxy even for partially applied THF equality, because
+                    the LEO-II and Satallax parsers complain about not being
+                    able to infer the type of "=". *)
+                 IConst (proxy_base |>> prefix const_prefix, T, T_args)
              | _ => IConst (name, T, [])
            else
              IConst (proxy_base |>> prefix const_prefix, T, T_args)
@@ -1918,9 +1960,36 @@
 val explicit_apply = NONE (* for experiments *)
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
-        exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
+        exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
     val (format, type_enc) = choose_format [format] type_enc
+    val lambda_trans =
+      if lambda_trans = smartN then
+        if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+      else if lambda_trans = lambdasN andalso
+              not (is_type_enc_higher_order type_enc) then
+        error ("Lambda translation method incompatible with first-order \
+               \encoding.")
+      else
+        lambda_trans
+    val trans_lambdas =
+      if lambda_trans = no_lambdasN then
+        rpair []
+      else if lambda_trans = concealedN then
+        lift_lambdas ctxt type_enc ##> K []
+      else if lambda_trans = liftingN then
+        lift_lambdas ctxt type_enc
+      else if lambda_trans = combinatorsN then
+        map (introduce_combinators ctxt) #> rpair []
+      else if lambda_trans = hybridN then
+        lift_lambdas ctxt type_enc
+        ##> maps (fn t => [t, introduce_combinators ctxt
+                                  (intentionalize_def t)])
+      else if lambda_trans = lambdasN then
+        map (Envir.eta_contract) #> rpair []
+      else
+        error ("Unknown lambda translation method: " ^
+               quote lambda_trans ^ ".")
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
                          hyp_ts concl_t facts
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -197,7 +197,7 @@
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
-                          (rpair []) false false [] @{prop False} props
+                          no_lambdasN false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -199,7 +199,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
 fun default_provers_param_value ctxt =
-  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
+  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
                                   max_default_remote_threads)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -60,12 +60,6 @@
   type prover =
     params -> (string -> minimize_command) -> prover_problem -> prover_result
 
-  val concealedN : string
-  val liftingN : string
-  val combinatorsN : string
-  val hybridN : string
-  val lambdasN : string
-  val smartN : string
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
@@ -335,13 +329,6 @@
 
 (* configuration attributes *)
 
-val concealedN = "concealed"
-val liftingN = "lifting"
-val combinatorsN = "combinators"
-val hybridN = "hybrid"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
 (* Empty string means create files in Isabelle's temporary files directory. *)
 val dest_dir =
   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
@@ -527,56 +514,6 @@
    | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
-fun lift_lambdas ctxt type_enc =
-  map (close_form o Envir.eta_contract) #> rpair ctxt
-  #-> Lambda_Lifting.lift_lambdas
-          (if polymorphism_of_type_enc type_enc = Polymorphic then
-             SOME polymorphic_free_prefix
-           else
-             NONE)
-          Lambda_Lifting.is_quantifier
-  #> fst
-
-fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
-    intentionalize_def t
-  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
-    let
-      fun lam T t = Abs (Name.uu, T, t)
-      val (head, args) = strip_comb t ||> rev
-      val head_T = fastype_of head
-      val n = length args
-      val arg_Ts = head_T |> binder_types |> take n |> rev
-      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
-    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
-  | intentionalize_def t = t
-
-fun translate_atp_lambdas ctxt type_enc =
-  Config.get ctxt atp_lambda_translation
-  |> (fn trans =>
-         if trans = smartN then
-           if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
-         else if trans = lambdasN andalso
-                 not (is_type_enc_higher_order type_enc) then
-           error ("Lambda translation method incompatible with first-order \
-                  \encoding.")
-         else
-           trans)
-  |> (fn trans =>
-         if trans = concealedN then
-           lift_lambdas ctxt type_enc ##> K []
-         else if trans = liftingN then
-           lift_lambdas ctxt type_enc
-         else if trans = combinatorsN then
-           map (introduce_combinators ctxt) #> rpair []
-         else if trans = hybridN then
-           lift_lambdas ctxt type_enc
-           ##> maps (fn t => [t, introduce_combinators ctxt
-                                     (intentionalize_def t)])
-         else if trans = lambdasN then
-           map (Envir.eta_contract) #> rpair []
-         else
-           error ("Unknown lambda translation method: " ^ quote trans ^ "."))
-
 val metis_minimize_max_time = seconds 2.0
 
 fun choose_minimize_command minimize_command name preplay =
@@ -708,7 +645,8 @@
                 val (atp_problem, pool, conjecture_offset, facts_offset,
                      fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                      type_enc sound false (translate_atp_lambdas ctxt type_enc)
+                      type_enc sound false
+                      (Config.get ctxt atp_lambda_translation)
                       (Config.get ctxt atp_readable_names) true hyp_ts concl_t
                       facts
                 fun weights () = atp_problem_weights atp_problem
--- a/src/Pure/Syntax/parser.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -747,7 +747,7 @@
   in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS ctxt warned prods chains Estate i c states =
+fun PROCESSS ctxt prods chains Estate i c states =
   let
     fun all_prods_for nt = prods_for prods chains true c [nt];
 
@@ -773,14 +773,6 @@
                         val tk_prods = all_prods_for nt;
                         val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
                       in (Inttab.update (nt, (min_prec, [])) used, States') end);
-
-                val _ =
-                  if not (! warned) andalso
-                     length new_states + length States > Config.get ctxt branching_level then
-                    (Context_Position.if_visible ctxt warning
-                      "Currently parsed expression could be extremely ambiguous";
-                     warned := true)
-                  else ();
               in
                 processS used' (new_states @ States) (S :: Si, Sii)
               end
@@ -803,7 +795,7 @@
   in processS Inttab.empty states ([], []) end;
 
 
-fun produce ctxt warned prods tags chains stateset i indata prev_token =
+fun produce ctxt prods tags chains stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
@@ -821,10 +813,10 @@
         [] => s
       | c :: cs =>
           let
-            val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
+            val (si, sii) = PROCESSS ctxt prods chains stateset i c s;
             val _ = Array.update (stateset, i, si);
             val _ = Array.update (stateset, i + 1, sii);
-          in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
+          in produce ctxt prods tags chains stateset (i + 1) cs c end));
 
 
 fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
@@ -841,7 +833,7 @@
     val _ = Array.update (Estate, 0, S0);
   in
     get_trees
-      (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
+      (produce ctxt prods tags chains Estate 0 indata Lexicon.eof)
   end;
 
 
--- a/src/Tools/eqsubst.ML	Tue Aug 09 08:07:22 2011 +0200
+++ b/src/Tools/eqsubst.ML	Tue Aug 09 18:52:18 2011 +0200
@@ -108,10 +108,6 @@
     val searchf_bt_unify_valid :
        searchinfo -> term -> match Seq.seq Seq.seq
 
-    (* syntax tools *)
-    val ith_syntax : int list parser
-    val options_syntax : bool parser
-
     (* Isar level hooks *)
     val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
     val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
@@ -546,23 +542,15 @@
 fun eqsubst_asm_meth ctxt occL inthms =
     SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
 
-(* syntax for options, given "(asm)" will give back true, without
-   gives back false *)
-val options_syntax =
-    (Args.parens (Args.$$$ "asm") >> (K true)) ||
-     (Scan.succeed false);
-
-val ith_syntax =
-    Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
-
 (* combination method that takes a flag (true indicates that subst
    should be done to an assumption, false = apply to the conclusion of
    the goal) as well as the theorems to use *)
 val setup =
   Method.setup @{binding subst}
-    (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
-      (fn ((asmflag, occL), inthms) => fn ctxt =>
-        (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
+    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+        Attrib.thms >>
+      (fn ((asm, occL), inthms) => fn ctxt =>
+        (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
     "single-step substitution";
 
 end;