1.1 --- a/TFL/tfl.ML	Tue Feb 19 23:49:49 2002 +0100
     1.2 +++ b/TFL/tfl.ML	Wed Feb 20 00:53:53 2002 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4        val vname = ref "u"
     1.5        fun new() =
     1.6           if !vname mem_string (!slist)
     1.7 -         then (vname := bump_string (!vname);  new())
     1.8 +         then (vname := Symbol.bump_string (!vname);  new())
     1.9           else (slist := !vname :: !slist;  !vname)
    1.10    in
    1.11    fn ty => Free(new(), ty)

     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Feb 19 23:49:49 2002 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Feb 20 00:53:53 2002 +0100
     2.3 @@ -421,7 +421,7 @@
     2.4            val ps = if_none (assoc (factors, P)) [];
     2.5            val Ts = prodT_factors [] ps T;
     2.6            val (frees, x') = foldr (fn (T', (fs, s)) =>
     2.7 -            ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
     2.8 +            ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
     2.9            val tuple = mk_tuple [] ps T frees;
    2.10        in ((HOLogic.mk_binop "op -->"
    2.11          (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')

     3.1 --- a/src/HOL/ex/SVC_Oracle.ML	Tue Feb 19 23:49:49 2002 +0100
     3.2 +++ b/src/HOL/ex/SVC_Oracle.ML	Wed Feb 20 00:53:53 2002 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4  	let val T = fastype_of t
     3.5              val v = Unify.combound (Var ((!vname,0), Us--->T),
     3.6  				    0, nPar)
     3.7 -	in  vname := bump_string (!vname); 
     3.8 +	in  vname := Symbol.bump_string (!vname); 
     3.9  	    pairs := (t, v) :: !pairs;
    3.10  	    v
    3.11  	end;

     4.1 --- a/src/Provers/blast.ML	Tue Feb 19 23:49:49 2002 +0100
     4.2 +++ b/src/Provers/blast.ML	Wed Feb 20 00:53:53 2002 +0100
     4.3 @@ -415,12 +415,12 @@
     4.4  (*A debugging function: replaces all Vars by dummy Frees for visual inspection
     4.5    of whether they are distinct.  Function revert undoes the assignments.*)
     4.6  fun instVars t =
     4.7 -  let val name = ref "A"
     4.8 +  let val name = ref "a"
     4.9        val updated = ref []
    4.10        fun inst (TConst(a,t)) = inst t
    4.11  	| inst (Var(v as ref None)) = (updated := v :: (!updated);
    4.12  				       v       := Some (Free ("?" ^ !name)); 
    4.13 -				       name    := bump_string (!name))
    4.14 +				       name    := Symbol.bump_string (!name))
    4.15  	| inst (Abs(a,t))    = inst t
    4.16  	| inst (f $ u)       = (inst f; inst u)
    4.17  	| inst _             = ()

     5.1 --- a/src/Pure/logic.ML	Tue Feb 19 23:49:49 2002 +0100
     5.2 +++ b/src/Pure/logic.ML	Wed Feb 20 00:53:53 2002 +0100
     5.3 @@ -306,7 +306,7 @@
     5.4      then res_inst_tac would not work properly.*)
     5.5  fun rename_vars (a, []) = []
     5.6    | rename_vars (a, (_,T)::vars) =
     5.7 -        (a,T) :: rename_vars (bump_string a, vars);
     5.8 +        (a,T) :: rename_vars (Symbol.bump_string a, vars);
     5.9  
    5.10  (*Move all parameters to the front of the subgoal, renaming them apart;
    5.11    if n>0 then deletes assumption n. *)

     6.1 --- a/src/Pure/term.ML	Tue Feb 19 23:49:49 2002 +0100
     6.2 +++ b/src/Pure/term.ML	Wed Feb 20 00:53:53 2002 +0100
     6.3 @@ -738,7 +738,7 @@
     6.4  fun variant bs name =
     6.5    let
     6.6      val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
     6.7 -    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (bump_string c) else c;
     6.8 +    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
     6.9      fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c;
    6.10    in vary1 (if c = "" then "u" else c) ^ u end;
    6.11  

     7.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Feb 19 23:49:49 2002 +0100
     7.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Feb 20 00:53:53 2002 +0100
     7.3 @@ -57,7 +57,7 @@
     7.4  
     7.5  (*make distinct individual variables a1, a2, a3, ..., an. *)
     7.6  fun mk_frees a [] = []
     7.7 -  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
     7.8 +  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts;
     7.9  
    7.10  
    7.11  (* add_inductive(_i) *)