# HG changeset patch
# User wenzelm
# Date 879348130 -3600
# Node ID cef5ef41e70d9d417ce077ccdc5837cf75e4349a
# Parent  68c7b37f8721b2dad1c402296d1b90f0311bdb41
tuned warning msg;

diff -r 68c7b37f8721 -r cef5ef41e70d src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Nov 12 16:21:57 1997 +0100
+++ b/src/Pure/tactic.ML	Wed Nov 12 16:22:10 1997 +0100
@@ -553,7 +553,7 @@
   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