# HG changeset patch # User wenzelm # Date 1369921915 -7200 # Node ID d84ff5a93764f6a60c7ab13b8b83250193af297e # Parent ab3ba550cbe798e92dff5e27e2508367f33d957f more standard names; diff -r ab3ba550cbe7 -r d84ff5a93764 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Thu May 30 15:02:33 2013 +0200 +++ b/src/Tools/eqsubst.ML Thu May 30 15:51:55 2013 +0200 @@ -296,12 +296,12 @@ SkipMore _ => Seq.empty | SkipSeq ss => Seq.flat ss); -(* The occL is a list of integers indicating which occurence +(* The "occs" argument is a list of integers indicating which occurence w.r.t. the search order, to rewrite. Backtracking will also find later occurences, but all earlier ones are skipped. Thus you can use [0] to just find all rewrites. *) -fun eqsubst_tac ctxt occL thms i st = +fun eqsubst_tac ctxt occs thms i st = let val nprems = Thm.nprems_of st in if nprems < i then Seq.empty else let @@ -311,9 +311,9 @@ eqsubst_tac' ctxt (skip_first_occs_search occ searchf_lr_unify_valid) r (i + (Thm.nprems_of st - nprems)) st); - val sortedoccL = Library.sort (rev_order o int_ord) occL; + val sorted_occs = Library.sort (rev_order o int_ord) occs; in - Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccL) st) + Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st) end end; @@ -395,20 +395,20 @@ fun skip_first_asm_occs_search searchf sinfo occ lhs = skipto_skipseq occ (searchf sinfo lhs); -fun eqsubst_asm_tac ctxt occL thms i st = +fun eqsubst_asm_tac ctxt occs thms i st = let val nprems = Thm.nprems_of st in if nprems < i then Seq.empty else let val thmseq = Seq.of_list thms; - fun apply_occ occK st = + fun apply_occ occ st = thmseq |> Seq.maps (fn r => eqsubst_asm_tac' ctxt - (skip_first_asm_occs_search searchf_lr_unify_valid) occK r + (skip_first_asm_occs_search searchf_lr_unify_valid) occ r (i + (Thm.nprems_of st - nprems)) st); - val sortedoccs = Library.sort (rev_order o int_ord) occL; + val sorted_occs = Library.sort (rev_order o int_ord) occs; in - Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccs) st) + Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st) end end; @@ -419,8 +419,8 @@ Method.setup @{binding subst} (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) -- Attrib.thms >> - (fn ((asm, occL), inthms) => fn ctxt => - SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occL inthms))) + (fn ((asm, occs), inthms) => fn ctxt => + SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms))) "single-step substitution"; end;