diff -r a0e4618d6fed -r 6cebeee3863e src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Mon Jun 18 17:50:06 2012 +0200
+++ b/src/Provers/hypsubst.ML	Tue Jun 19 11:18:09 2012 +0200
@@ -2,7 +2,7 @@
     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     Copyright   1995  University of Cambridge
 
-Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
+Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst".
 
 Tactic to substitute using (at least) the assumption x=t in the rest
 of the subgoal, and to delete (at least) that assumption.  Original