src/Pure/tactic.ML
changeset 25939 ddea202704b4
parent 24244 d7ee11ba1534
child 26424 a6cad32a27b0
     1.1 --- a/src/Pure/tactic.ML	Mon Jan 21 08:45:36 2008 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Jan 21 14:18:49 2008 +0100
     1.3 @@ -506,11 +506,7 @@
     1.4  fun rename_params_tac xs i =
     1.5    case Library.find_first (not o Syntax.is_identifier) xs of
     1.6        SOME x => error ("Not an identifier: " ^ x)
     1.7 -    | NONE =>
     1.8 -       (if !Logic.auto_rename
     1.9 -         then (warning "Resetting Logic.auto_rename";
    1.10 -             Logic.auto_rename := false)
    1.11 -        else (); PRIMITIVE (rename_params_rule (xs, i)));
    1.12 +    | NONE => PRIMITIVE (rename_params_rule (xs, i));
    1.13  
    1.14  (*scan a list of characters into "words" composed of "letters" (recognized by
    1.15    is_let) and separated by any number of non-"letters"*)