| changeset 12902 | a23dc0b7566f |
| parent 12876 | a70df1e5bf10 |
| child 13627 | 67b0b7500a9d |
--- 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) *)