--- a/src/Pure/Isar/method.ML Wed Apr 04 00:11:17 2007 +0200
+++ b/src/Pure/Isar/method.ML Wed Apr 04 00:11:18 2007 +0200
@@ -567,7 +567,7 @@
("fact", thms_ctxt_args fact, "composition by facts from context"),
("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
- "rename parameters of goal (dynamic instantiation)"),
+ "rename parameters of goal"),
("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
"rotate assumptions of goal"),
("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);