diff -r 748f4e365d14 -r 2e47ea2c6109 src/Pure/tactic.ML
--- 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;