tuned warning msg;
authorwenzelm
Wed Nov 12 16:22:10 1997 +0100 (1997-11-12)
changeset 4213cef5ef41e70d
parent 4212 68c7b37f8721
child 4214 523f6bea9fd7
tuned warning msg;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Wed Nov 12 16:21:57 1997 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Nov 12 16:22:10 1997 +0100
     1.3 @@ -553,7 +553,7 @@
     1.4    let val cs = explode str 
     1.5    in  
     1.6    if !Logic.auto_rename 
     1.7 -  then (writeln"Note: setting Logic.auto_rename := false"; 
     1.8 +  then (warning "Resetting Logic.auto_rename"; 
     1.9  	Logic.auto_rename := false)
    1.10    else ();
    1.11    case #2 (take_prefix (is_letdig orf is_blank) cs) of