diff options
Diffstat (limited to 'spartan/core/eqsubst.ML')
| -rw-r--r-- | spartan/core/eqsubst.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML index e7ecf63..31d5126 100644 --- a/spartan/core/eqsubst.ML +++ b/spartan/core/eqsubst.ML @@ -433,7 +433,7 @@ val _ = "single-step substitution" #> Method.setup \<^binding>\<open>subst\<close> (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS + CHEADGOAL o SIDE_CONDS 0 ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms))))) "single-step substitution with automatic discharge of side conditions" ) |