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