# HG changeset patch
# User wenzelm
# Date 1369918953 -7200
# Node ID ab3ba550cbe798e92dff5e27e2508367f33d957f
# Parent  fb82b42eb49873df978fea6dce33336170475365
simplified method setup;

diff -r fb82b42eb498 -r ab3ba550cbe7 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Thu May 30 14:37:06 2013 +0200
+++ b/src/Tools/eqsubst.ML	Thu May 30 15:02:33 2013 +0200
@@ -82,7 +82,7 @@
     fun skip_occs n sq =
       (case Seq.pull sq of
         NONE => SkipMore n
-      | SOME (h,t) =>
+      | SOME (h, t) =>
         (case Seq.pull h of
           NONE => skip_occs n t
         | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
@@ -318,10 +318,6 @@
   end;
 
 
-(* inthms are the given arguments in Isar, and treated as eqstep with
-   the first one, then the second etc *)
-fun eqsubst_meth ctxt occL inthms = SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
-
 (* apply a substitution inside assumption j, keeps asm in the same place *)
 fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
   let
@@ -416,11 +412,6 @@
       end
   end;
 
-(* inthms are the given arguments in Isar, and treated as eqstep with
-   the first one, then the second etc *)
-fun eqsubst_asm_meth ctxt occL inthms =
-  SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
-
 (* combination method that takes a flag (true indicates that subst
    should be done to an assumption, false = apply to the conclusion of
    the goal) as well as the theorems to use *)
@@ -429,7 +420,7 @@
     (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
         Attrib.thms >>
       (fn ((asm, occL), inthms) => fn ctxt =>
-        (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
+        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occL inthms)))
     "single-step substitution";
 
 end;