src/Pure/tactic.ML

   it affects nothing but the names of bound variables!*)
 fun rename_tac str i = 
   let val cs = explode str 
   in  
   if !Logic.auto_rename 
-  then (writeln"Note: setting Logic.auto_rename := false"; 
+  then (warning "Resetting Logic.auto_rename"; 
 	Logic.auto_rename := false)
   else ();
   case #2 (take_prefix (is_letdig orf is_blank) cs) of
       [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
     | c::_ => error ("Illegal character: " ^ c)