equal
deleted
inserted
replaced
166 full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1 |
166 full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1 |
167 else full_simp_tac dist_ss 1); |
167 else full_simp_tac dist_ss 1); |
168 |
168 |
169 val inject = map (fn r => r RS iffD1) |
169 val inject = map (fn r => r RS iffD1) |
170 (if i < length newTs then List.nth (constr_inject, i) |
170 (if i < length newTs then List.nth (constr_inject, i) |
171 else #inject (valOf (Symtab.lookup (dt_info, tname)))); |
171 else #inject (the (Symtab.curried_lookup dt_info tname))); |
172 |
172 |
173 fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) = |
173 fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) = |
174 let |
174 let |
175 val k = length (List.filter is_rec_type cargs) |
175 val k = length (List.filter is_rec_type cargs) |
176 |
176 |