src/Tools/eqsubst.ML
changeset 52237 ab3ba550cbe7
parent 52236 fb82b42eb498
child 52238 d84ff5a93764
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 14:37:06 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 15:02:33 2013 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4      fun skip_occs n sq =
     1.5        (case Seq.pull sq of
     1.6          NONE => SkipMore n
     1.7 -      | SOME (h,t) =>
     1.8 +      | SOME (h, t) =>
     1.9          (case Seq.pull h of
    1.10            NONE => skip_occs n t
    1.11          | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
    1.12 @@ -318,10 +318,6 @@
    1.13    end;
    1.14  
    1.15  
    1.16 -(* inthms are the given arguments in Isar, and treated as eqstep with
    1.17 -   the first one, then the second etc *)
    1.18 -fun eqsubst_meth ctxt occL inthms = SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
    1.19 -
    1.20  (* apply a substitution inside assumption j, keeps asm in the same place *)
    1.21  fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
    1.22    let
    1.23 @@ -416,11 +412,6 @@
    1.24        end
    1.25    end;
    1.26  
    1.27 -(* inthms are the given arguments in Isar, and treated as eqstep with
    1.28 -   the first one, then the second etc *)
    1.29 -fun eqsubst_asm_meth ctxt occL inthms =
    1.30 -  SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
    1.31 -
    1.32  (* combination method that takes a flag (true indicates that subst
    1.33     should be done to an assumption, false = apply to the conclusion of
    1.34     the goal) as well as the theorems to use *)
    1.35 @@ -429,7 +420,7 @@
    1.36      (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
    1.37          Attrib.thms >>
    1.38        (fn ((asm, occL), inthms) => fn ctxt =>
    1.39 -        (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
    1.40 +        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occL inthms)))
    1.41      "single-step substitution";
    1.42  
    1.43  end;