equal
deleted
inserted
replaced
145 val recursor = head_of (#1 (hd recursor_pairs)) |
145 val recursor = head_of (#1 (hd recursor_pairs)) |
146 |
146 |
147 (** make definition **) |
147 (** make definition **) |
148 |
148 |
149 (*the recursive argument*) |
149 (*the recursive argument*) |
150 val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name), |
150 val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name), |
151 Ind_Syntax.iT) |
151 Ind_Syntax.iT) |
152 |
152 |
153 val def_tm = Logic.mk_equals |
153 val def_tm = Logic.mk_equals |
154 (subst_bound (rec_arg, fabs), |
154 (subst_bound (rec_arg, fabs), |
155 list_comb (recursor, |
155 list_comb (recursor, |