# HG changeset patch
# User wenzelm
# Date 1309179835 -7200
# Node ID c1966f3221059c9a5d028d1b2f5c7d3ee4e9509d
# Parent  94a08fb3ae4a7774d6fe3ffda688b1f922298485
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;

diff -r 94a08fb3ae4a -r c1966f322105 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 15:01:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 15:03:55 2011 +0200
@@ -320,7 +320,7 @@
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
             add_pconst_to_table true
-                (gensym skolem_prefix, PType (order_of_type abs_T, []))
+                (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula ext_arg T =
diff -r 94a08fb3ae4a -r c1966f322105 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jun 27 15:01:08 2011 +0200
+++ b/src/Pure/drule.ML	Mon Jun 27 15:03:55 2011 +0200
@@ -313,7 +313,7 @@
    case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
        [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
-         let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
+         let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix))
              val alist = map newName vars
              fun mk_inst (Var(v,T)) =
                  (cterm_of thy (Var(v,T)),
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;