src/Provers/eqsubst.ML

   #> (fn (ctxt, ((asmflag, occL), inthms)) =>
     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
 
 
 val setup =
-  Method.add_method ("subst", subst_meth, "substiution with an equation");
+  Method.add_method ("subst", subst_meth, "single-step substitution");
 
 end;