diff -r 2c1c0e989615 -r ddea202704b4 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Jan 21 08:45:36 2008 +0100
+++ b/src/Pure/tactic.ML	Mon Jan 21 14:18:49 2008 +0100
@@ -506,11 +506,7 @@
 fun rename_params_tac xs i =
   case Library.find_first (not o Syntax.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)
-    | NONE =>
-       (if !Logic.auto_rename
-         then (warning "Resetting Logic.auto_rename";
-             Logic.auto_rename := false)
-        else (); PRIMITIVE (rename_params_rule (xs, i)));
+    | NONE => PRIMITIVE (rename_params_rule (xs, i));
 
 (*scan a list of characters into "words" composed of "letters" (recognized by
   is_let) and separated by any number of non-"letters"*)