tuned warning msg;
authorwenzelm
Wed, 12 Nov 1997 16:22:10 +0100
changeset 4213 cef5ef41e70d
parent 4212 68c7b37f8721
child 4214 523f6bea9fd7
tuned warning msg;
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