diff options
Diffstat (limited to 'spartan/core/rewrite.ML')
| -rw-r--r-- | spartan/core/rewrite.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index eba0e81..99c21b5 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -458,7 +458,7 @@ val _ = "single-step rewriting, allowing subterm selection via patterns" #> Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >> (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS + CHEADGOAL o SIDE_CONDS 0 (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) "single-step rewriting with auto-typechecking" end |