adapted to baroque chars;

--- 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";
 

--- a/src/Pure/tactic.ML	Mon Mar 09 16:08:37 1998 +0100
+++ b/src/Pure/tactic.ML	Mon Mar 09 16:09:06 1998 +0100
@@ -528,14 +528,14 @@
 (*Calling this will generate the warning "Same as previous level" since
   it affects nothing but the names of bound variables!*)
 fun rename_tac str i = 
-  let val cs = explode str 
+  let val cs = Symbol.explode str 
   in  
   if !Logic.auto_rename 
   then (warning "Resetting Logic.auto_rename"; 
 	Logic.auto_rename := false)
   else ();
-  case #2 (take_prefix (is_letdig orf is_blank) cs) of
-      [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
+  case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
+      [] => PRIMITIVE (rename_params_rule (scanwords Symbol.is_letdig cs, i))
     | c::_ => error ("Illegal character: " ^ c)
   end;