more standard names;
authorwenzelm
Thu May 30 15:51:55 2013 +0200 (2013-05-30)
changeset 52238d84ff5a93764
parent 52237 ab3ba550cbe7
child 52239 6a6033fa507c
more standard names;
src/Tools/eqsubst.ML
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 15:02:33 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 15:51:55 2013 +0200
     1.3 @@ -296,12 +296,12 @@
     1.4      SkipMore _ => Seq.empty
     1.5    | SkipSeq ss => Seq.flat ss);
     1.6  
     1.7 -(* The occL is a list of integers indicating which occurence
     1.8 +(* The "occs" argument is a list of integers indicating which occurence
     1.9  w.r.t. the search order, to rewrite. Backtracking will also find later
    1.10  occurences, but all earlier ones are skipped. Thus you can use [0] to
    1.11  just find all rewrites. *)
    1.12  
    1.13 -fun eqsubst_tac ctxt occL thms i st =
    1.14 +fun eqsubst_tac ctxt occs thms i st =
    1.15    let val nprems = Thm.nprems_of st in
    1.16      if nprems < i then Seq.empty else
    1.17      let
    1.18 @@ -311,9 +311,9 @@
    1.19            eqsubst_tac' ctxt
    1.20              (skip_first_occs_search occ searchf_lr_unify_valid) r
    1.21              (i + (Thm.nprems_of st - nprems)) st);
    1.22 -      val sortedoccL = Library.sort (rev_order o int_ord) occL;
    1.23 +      val sorted_occs = Library.sort (rev_order o int_ord) occs;
    1.24      in
    1.25 -      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccL) st)
    1.26 +      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
    1.27      end
    1.28    end;
    1.29  
    1.30 @@ -395,20 +395,20 @@
    1.31  fun skip_first_asm_occs_search searchf sinfo occ lhs =
    1.32    skipto_skipseq occ (searchf sinfo lhs);
    1.33  
    1.34 -fun eqsubst_asm_tac ctxt occL thms i st =
    1.35 +fun eqsubst_asm_tac ctxt occs thms i st =
    1.36    let val nprems = Thm.nprems_of st in
    1.37      if nprems < i then Seq.empty
    1.38      else
    1.39        let
    1.40          val thmseq = Seq.of_list thms;
    1.41 -        fun apply_occ occK st =
    1.42 +        fun apply_occ occ st =
    1.43            thmseq |> Seq.maps (fn r =>
    1.44              eqsubst_asm_tac' ctxt
    1.45 -              (skip_first_asm_occs_search searchf_lr_unify_valid) occK r
    1.46 +              (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
    1.47                (i + (Thm.nprems_of st - nprems)) st);
    1.48 -        val sortedoccs = Library.sort (rev_order o int_ord) occL;
    1.49 +        val sorted_occs = Library.sort (rev_order o int_ord) occs;
    1.50        in
    1.51 -        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sortedoccs) st)
    1.52 +        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
    1.53        end
    1.54    end;
    1.55  
    1.56 @@ -419,8 +419,8 @@
    1.57    Method.setup @{binding subst}
    1.58      (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
    1.59          Attrib.thms >>
    1.60 -      (fn ((asm, occL), inthms) => fn ctxt =>
    1.61 -        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occL inthms)))
    1.62 +      (fn ((asm, occs), inthms) => fn ctxt =>
    1.63 +        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
    1.64      "single-step substitution";
    1.65  
    1.66  end;