--- 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)
--- 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')
--- 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;
--- 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 _ = ()
--- 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. *)
--- 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;
--- 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) *)