diff options
Diffstat (limited to 'spartan/core/rewrite.ML')
-rw-r--r-- | spartan/core/rewrite.ML | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index f9c5d8e..eba0e81 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -15,8 +15,8 @@ patterns but has diverged significantly during its development. We also allow introduction of identifiers for bound variables, which can then be used to match arbitrary subterms inside abstractions. -This code is slightly modified from the original at HOL/Library/rewrite.ML, -to incorporate auto-typechecking for type theory. +This code has been slightly modified from the original at HOL/Library/rewrite.ML +to incorporate automatic discharge of type-theoretic side conditions. *) infix 1 then_pconv; @@ -448,18 +448,18 @@ val _ = val subst_parser = let val scan = raw_pattern -- to_parser -- Parse.thms1 in context_lift scan prep_args end + + fun rewrite_export_ctac inputs inthms = + CONTEXT_TACTIC' (fn ctxt => rewrite_export_tac ctxt inputs inthms) in Method.setup \<^binding>\<open>rewr\<close> (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => - SIMPLE_METHOD' - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) - "single-step rewriting, allowing subterm selection via patterns" - #> - (Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => - SIMPLE_METHOD' (SIDE_CONDS - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms) - orig_ctxt))) - "single-step rewriting with auto-typechecking") + (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD' + (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) + "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 + (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) + "single-step rewriting with auto-typechecking" end end |