src/HOL/Tools/inductive_package.ML
changeset 12902 a23dc0b7566f
parent 12876 a70df1e5bf10
child 12922 ed70a600f0ea
     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')