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