diff -r 94a08fb3ae4a -r c1966f322105 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jun 27 15:01:08 2011 +0200
+++ b/src/Pure/library.ML	Mon Jun 27 15:03:55 2011 +0200
@@ -211,7 +211,7 @@
     'a -> 'b -> 'c * 'b
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
-  val gensym: string -> string
+  val legacy_gensym: string -> string
   type stamp = unit Unsynchronized.ref
   val stamp: unit -> stamp
   type serial = int
@@ -1043,9 +1043,8 @@
 
 
 
-(* generating identifiers *)
+(* generating identifiers -- often fresh *)
 
-(** Freshly generated identifiers; supplied prefix MUST start with a letter **)
 local
 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
 fun gensym_char i =
@@ -1059,8 +1058,8 @@
 val gensym_seed = Unsynchronized.ref (0: int);
 
 in
-  fun gensym pre =
-    pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
+  fun legacy_gensym pre =
+    pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed));
 end;