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')