139 | SOME (ls, cargs', rs, rhs, eq) => |
139 | SOME (ls, cargs', rs, rhs, eq) => |
140 let |
140 let |
141 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
141 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
142 val rargs = map fst recs; |
142 val rargs = map fst recs; |
143 val subs = map (rpair dummyT o fst) |
143 val subs = map (rpair dummyT o fst) |
144 (rev (rename_wrt_term rhs rargs)); |
144 (rev (Term.rename_wrt_term rhs rargs)); |
145 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
145 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
146 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
146 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
147 handle PrimrecError (s, NONE) => primrec_error_eqn s eq |
147 handle PrimrecError (s, NONE) => primrec_error_eqn s eq |
148 in (fnames'', fnss'', |
148 in (fnames'', fnss'', |
149 (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns) |
149 (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns) |