--- a/src/Pure/term.ML Wed Oct 30 11:17:54 1996 +0100
+++ b/src/Pure/term.ML Wed Oct 30 11:19:09 1996 +0100
@@ -472,8 +472,8 @@
(*Makes a variant of the name c distinct from the names in bs.
First attaches the suffix "a" and then increments this. *)
fun variant bs c : string =
- let fun vary2 c = if (c mem bs) then vary2 (bump_string c) else c
- fun vary1 c = if (c mem bs) then vary2 (c ^ "a") else c
+ let fun vary2 c = if (c mem_string bs) then vary2 (bump_string c) else c
+ fun vary1 c = if (c mem_string bs) then vary2 (c ^ "a") else c
in vary1 (if c="" then "u" else c) end;
(*Create variants of the list of names, with priority to the first ones*)