1.1 --- a/src/HOL/Hoare/HoareAbort.thy	Mon Jun 16 22:13:50 2008 +0200
     1.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Mon Jun 16 22:13:52 2008 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4                rtac CollectI i,
     1.5                dtac CollectD i,
     1.6                (TRY(split_all_tac i)) THEN_MAYBE
     1.7 -              ((rename_params_tac var_names i) THEN
     1.8 +              ((rename_tac var_names i) THEN
     1.9                 (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
    1.10    end;
    1.11  

     2.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 16 22:13:50 2008 +0200
     2.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 16 22:13:52 2008 +0200
     2.3 @@ -112,7 +112,7 @@
     2.4               rtac CollectI i,
     2.5               dtac CollectD i,
     2.6               (TRY(split_all_tac i)) THEN_MAYBE
     2.7 -             ((rename_params_tac var_names i) THEN
     2.8 +             ((rename_tac var_names i) THEN
     2.9                (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
    2.10    end;
    2.11  

     3.1 --- a/src/Pure/Isar/method.ML	Mon Jun 16 22:13:50 2008 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Mon Jun 16 22:13:52 2008 +0200
     3.3 @@ -592,7 +592,7 @@
     3.4      ("this", no_args this, "apply current facts as rules"),
     3.5      ("fact", thms_ctxt_args fact, "composition by facts from context"),
     3.6      ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
     3.7 -    ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
     3.8 +    ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac,
     3.9        "rename parameters of goal"),
    3.10      ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
    3.11        "rotate assumptions of goal"),