--- a/src/HOL/Hoare/HoareAbort.thy Mon Jun 16 22:13:50 2008 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy Mon Jun 16 22:13:52 2008 +0200
@@ -350,7 +350,7 @@
rtac CollectI i,
dtac CollectD i,
(TRY(split_all_tac i)) THEN_MAYBE
- ((rename_params_tac var_names i) THEN
+ ((rename_tac var_names i) THEN
(full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
end;
--- a/src/HOL/Hoare/hoare_tac.ML Mon Jun 16 22:13:50 2008 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Mon Jun 16 22:13:52 2008 +0200
@@ -112,7 +112,7 @@
rtac CollectI i,
dtac CollectD i,
(TRY(split_all_tac i)) THEN_MAYBE
- ((rename_params_tac var_names i) THEN
+ ((rename_tac var_names i) THEN
(full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
end;
--- a/src/Pure/Isar/method.ML Mon Jun 16 22:13:50 2008 +0200
+++ b/src/Pure/Isar/method.ML Mon Jun 16 22:13:52 2008 +0200
@@ -592,7 +592,7 @@
("this", no_args this, "apply current facts as rules"),
("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_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac,
"rename parameters of goal"),
("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
"rotate assumptions of goal"),