1.1 --- a/src/HOL/Tools/inductive_package.ML Tue Feb 19 23:49:49 2002 +0100
1.2 +++ b/src/HOL/Tools/inductive_package.ML Wed Feb 20 00:53:53 2002 +0100
1.3 @@ -421,7 +421,7 @@
1.4 val ps = if_none (assoc (factors, P)) [];
1.5 val Ts = prodT_factors [] ps T;
1.6 val (frees, x') = foldr (fn (T', (fs, s)) =>
1.7 - ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
1.8 + ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
1.9 val tuple = mk_tuple [] ps T frees;
1.10 in ((HOLogic.mk_binop "op -->"
1.11 (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')