1.1 --- a/src/Pure/logic.ML	Mon Mar 09 16:08:37 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Mon Mar 09 16:09:06 1998 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  
     1.5  (*rename_prefix is not exported; it is set by this function.*)
     1.6  fun set_rename_prefix a =
     1.7 -    if a<>"" andalso forall is_letter (explode a)
     1.8 +    if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
     1.9      then  (rename_prefix := a;  auto_rename := true)
    1.10      else  error"rename prefix must be nonempty and consist of letters";
    1.11