153 | SOME (ls, cargs', rs, rhs, eq) => |
153 | SOME (ls, cargs', rs, rhs, eq) => |
154 let |
154 let |
155 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
155 val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); |
156 val rargs = map fst recs; |
156 val rargs = map fst recs; |
157 val subs = map (rpair dummyT o fst) |
157 val subs = map (rpair dummyT o fst) |
158 (rev (rename_wrt_term rhs rargs)); |
158 (rev (Term.rename_wrt_term rhs rargs)); |
159 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
159 val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => |
160 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
160 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss') |
161 handle RecError s => primrec_eq_err lthy s eq |
161 handle RecError s => primrec_eq_err lthy s eq |
162 in (fnames'', fnss'', |
162 in (fnames'', fnss'', |
163 (list_abs_free (cargs' @ subs, rhs'))::fns) |
163 (list_abs_free (cargs' @ subs, rhs'))::fns) |