equal
deleted
inserted
replaced
55 |
55 |
56 (* utils *) |
56 (* utils *) |
57 |
57 |
58 (*make distinct individual variables a1, a2, a3, ..., an. *) |
58 (*make distinct individual variables a1, a2, a3, ..., an. *) |
59 fun mk_frees a [] = [] |
59 fun mk_frees a [] = [] |
60 | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts; |
60 | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts; |
61 |
61 |
62 |
62 |
63 (* add_inductive(_i) *) |
63 (* add_inductive(_i) *) |
64 |
64 |
65 (*internal version, accepting terms*) |
65 (*internal version, accepting terms*) |