--- 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"*)