# HG changeset patch
# User wenzelm
# Date 1014162833 -3600
# Node ID a23dc0b7566f40eb54e7b7db98b3ea2f2541b1bc
# Parent  4570584fbda95ed0699c65d31caf2085445a6fb7
Symbol.bump_string;

diff -r 4570584fbda9 -r a23dc0b7566f TFL/tfl.ML
--- a/TFL/tfl.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/TFL/tfl.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -82,7 +82,7 @@
       val vname = ref "u"
       fun new() =
          if !vname mem_string (!slist)
-         then (vname := bump_string (!vname);  new())
+         then (vname := Symbol.bump_string (!vname);  new())
          else (slist := !vname :: !slist;  !vname)
   in
   fn ty => Free(new(), ty)
diff -r 4570584fbda9 -r a23dc0b7566f src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -421,7 +421,7 @@
           val ps = if_none (assoc (factors, P)) [];
           val Ts = prodT_factors [] ps T;
           val (frees, x') = foldr (fn (T', (fs, s)) =>
-            ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
+            ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
           val tuple = mk_tuple [] ps T frees;
       in ((HOLogic.mk_binop "op -->"
         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
diff -r 4570584fbda9 -r a23dc0b7566f src/HOL/ex/SVC_Oracle.ML
--- a/src/HOL/ex/SVC_Oracle.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/HOL/ex/SVC_Oracle.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -30,7 +30,7 @@
 	let val T = fastype_of t
             val v = Unify.combound (Var ((!vname,0), Us--->T),
 				    0, nPar)
-	in  vname := bump_string (!vname); 
+	in  vname := Symbol.bump_string (!vname); 
 	    pairs := (t, v) :: !pairs;
 	    v
 	end;
diff -r 4570584fbda9 -r a23dc0b7566f src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/Provers/blast.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -415,12 +415,12 @@
 (*A debugging function: replaces all Vars by dummy Frees for visual inspection
   of whether they are distinct.  Function revert undoes the assignments.*)
 fun instVars t =
-  let val name = ref "A"
+  let val name = ref "a"
       val updated = ref []
       fun inst (TConst(a,t)) = inst t
 	| inst (Var(v as ref None)) = (updated := v :: (!updated);
 				       v       := Some (Free ("?" ^ !name)); 
-				       name    := bump_string (!name))
+				       name    := Symbol.bump_string (!name))
 	| inst (Abs(a,t))    = inst t
 	| inst (f $ u)       = (inst f; inst u)
 	| inst _             = ()
diff -r 4570584fbda9 -r a23dc0b7566f src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/Pure/logic.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -306,7 +306,7 @@
     then res_inst_tac would not work properly.*)
 fun rename_vars (a, []) = []
   | rename_vars (a, (_,T)::vars) =
-        (a,T) :: rename_vars (bump_string a, vars);
+        (a,T) :: rename_vars (Symbol.bump_string a, vars);
 
 (*Move all parameters to the front of the subgoal, renaming them apart;
   if n>0 then deletes assumption n. *)
diff -r 4570584fbda9 -r a23dc0b7566f src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/Pure/term.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -738,7 +738,7 @@
 fun variant bs name =
   let
     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
-    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (bump_string c) else c;
+    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
     fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c;
   in vary1 (if c = "" then "u" else c) ^ u end;
 
diff -r 4570584fbda9 -r a23dc0b7566f src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -57,7 +57,7 @@
 
 (*make distinct individual variables a1, a2, a3, ..., an. *)
 fun mk_frees a [] = []
-  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
+  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts;
 
 
 (* add_inductive(_i) *)