changeset 4693 | 2e47ea2c6109 |
parent 4679 | 24917efb31b5 |
child 4822 | 2733e21814fe |
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