--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 16:34:49 2011 +0200
@@ -205,7 +205,7 @@
(filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
(Symbol.explode name)))
val name'' = f (if name' = "" then empty else name')
- in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+ in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
(** constant table **)