old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
authorwenzelm
Mon Jun 27 15:03:55 2011 +0200 (2011-06-27)
changeset 43559c1966f322105
parent 43558 94a08fb3ae4a
child 43560 d1650e3720fd
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/Pure/drule.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 15:01:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 15:03:55 2011 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4        do_formula pos body_t
     1.5        #> (if also_skolems andalso will_surely_be_skolemized then
     1.6              add_pconst_to_table true
     1.7 -                (gensym skolem_prefix, PType (order_of_type abs_T, []))
     1.8 +                (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
     1.9            else
    1.10              I)
    1.11      and do_term_or_formula ext_arg T =
     2.1 --- a/src/Pure/drule.ML	Mon Jun 27 15:01:08 2011 +0200
     2.2 +++ b/src/Pure/drule.ML	Mon Jun 27 15:03:55 2011 +0200
     2.3 @@ -313,7 +313,7 @@
     2.4     case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
     2.5         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
     2.6       | vars =>
     2.7 -         let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
     2.8 +         let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix))
     2.9               val alist = map newName vars
    2.10               fun mk_inst (Var(v,T)) =
    2.11                   (cterm_of thy (Var(v,T)),
     3.1 --- a/src/Pure/library.ML	Mon Jun 27 15:01:08 2011 +0200
     3.2 +++ b/src/Pure/library.ML	Mon Jun 27 15:03:55 2011 +0200
     3.3 @@ -211,7 +211,7 @@
     3.4      'a -> 'b -> 'c * 'b
     3.5    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
     3.6    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
     3.7 -  val gensym: string -> string
     3.8 +  val legacy_gensym: string -> string
     3.9    type stamp = unit Unsynchronized.ref
    3.10    val stamp: unit -> stamp
    3.11    type serial = int
    3.12 @@ -1043,9 +1043,8 @@
    3.13  
    3.14  
    3.15  
    3.16 -(* generating identifiers *)
    3.17 +(* generating identifiers -- often fresh *)
    3.18  
    3.19 -(** Freshly generated identifiers; supplied prefix MUST start with a letter **)
    3.20  local
    3.21  (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
    3.22  fun gensym_char i =
    3.23 @@ -1059,8 +1058,8 @@
    3.24  val gensym_seed = Unsynchronized.ref (0: int);
    3.25  
    3.26  in
    3.27 -  fun gensym pre =
    3.28 -    pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
    3.29 +  fun legacy_gensym pre =
    3.30 +    pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed));
    3.31  end;
    3.32  
    3.33