src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Sat Oct 15 00:07:59 2005 +0200
+++ b/src/Pure/tactic.ML	Sat Oct 15 00:08:00 2005 +0200
@@ -588,8 +588,6 @@
      Names may contain letters, digits or primes and must be
      separated by blanks ***)
 
-(*Calling this will generate the warning "Same as previous level" since
-  it affects nothing but the names of bound variables!*)
 fun rename_params_tac xs i =
   case Library.find_first (not o Syntax.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)