renamed rename_params_tac to rename_tac;
authorwenzelm
Mon, 16 Jun 2008 22:13:52 +0200
changeset 27244 af0a44372d1f
parent 27243 d549b5b0f344
child 27245 817d34377170
renamed rename_params_tac to rename_tac;
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/hoare_tac.ML
src/Pure/Isar/method.ML
--- 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"),