src/Pure/tactic.ML
changeset 17851 2fa4f9b54761
parent 17496 26535df536ae
child 17892 62c397c17d18
     1.1 --- a/src/Pure/tactic.ML	Sat Oct 15 00:07:59 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Oct 15 00:08:00 2005 +0200
     1.3 @@ -588,8 +588,6 @@
     1.4       Names may contain letters, digits or primes and must be
     1.5       separated by blanks ***)
     1.6  
     1.7 -(*Calling this will generate the warning "Same as previous level" since
     1.8 -  it affects nothing but the names of bound variables!*)
     1.9  fun rename_params_tac xs i =
    1.10    case Library.find_first (not o Syntax.is_identifier) xs of
    1.11        SOME x => error ("Not an identifier: " ^ x)