diff -r 748f4e365d14 -r 2e47ea2c6109 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Mar 09 16:08:37 1998 +0100
+++ b/src/Pure/logic.ML	Mon Mar 09 16:09:06 1998 +0100
@@ -231,7 +231,7 @@
 
 (*rename_prefix is not exported; it is set by this function.*)
 fun set_rename_prefix a =
-    if a<>"" andalso forall is_letter (explode a)
+    if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
     then  (rename_prefix := a;  auto_rename := true)
     else  error"rename prefix must be nonempty and consist of letters";