# HG changeset patch
# User wenzelm
# Date 1213647232 -7200
# Node ID af0a44372d1f8c4eeb9d3d3ec8e979eb18e7336c
# Parent  d549b5b0f344b81e82436e1430c639d2ba363589
renamed rename_params_tac to rename_tac;

diff -r d549b5b0f344 -r af0a44372d1f src/HOL/Hoare/HoareAbort.thy
--- 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;
 
diff -r d549b5b0f344 -r af0a44372d1f src/HOL/Hoare/hoare_tac.ML
--- 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;
 
diff -r d549b5b0f344 -r af0a44372d1f src/Pure/Isar/method.ML
--- 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"),