191 alt_names : string list option, |
191 alt_names : string list option, |
192 descr : descr, |
192 descr : descr, |
193 sorts : (string * sort) list, |
193 sorts : (string * sort) list, |
194 inject : thm list, |
194 inject : thm list, |
195 distinct : simproc_dist, |
195 distinct : simproc_dist, |
196 inducts : thm list * thm, |
196 induct : thm, |
|
197 inducts : thm list, |
197 exhaust : thm, |
198 exhaust : thm, |
198 nchotomy : thm, |
199 nchotomy : thm, |
199 rec_names : string list, |
200 rec_names : string list, |
200 rec_rewrites : thm list, |
201 rec_rewrites : thm list, |
201 case_name : string, |
202 case_name : string, |
202 case_rewrites : thm list, |
203 case_rewrites : thm list, |
203 case_cong : thm, |
204 case_cong : thm, |
204 weak_case_cong : thm, |
205 weak_case_cong : thm, |
205 splits : thm * thm}; |
206 split : thm, |
|
207 split_asm: thm}; |
206 |
208 |
207 fun mk_Free s T i = Free (s ^ (string_of_int i), T); |
209 fun mk_Free s T i = Free (s ^ (string_of_int i), T); |
208 |
210 |
209 fun subst_DtTFree _ substs (T as (DtTFree name)) = |
211 fun subst_DtTFree _ substs (T as (DtTFree name)) = |
210 AList.lookup (op =) substs name |> the_default T |
212 AList.lookup (op =) substs name |> the_default T |