equal
deleted
inserted
replaced
261 let |
261 let |
262 val descr' = flat descr; |
262 val descr' = flat descr; |
263 val recTs = Datatype_Aux.get_rec_types descr' sorts; |
263 val recTs = Datatype_Aux.get_rec_types descr' sorts; |
264 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; |
264 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; |
265 val newTs = take (length (hd descr)) recTs; |
265 val newTs = take (length (hd descr)) recTs; |
266 val T' = TFree (Name.variant used "'t", HOLogic.typeS); |
266 val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS); |
267 |
267 |
268 val case_fn_Ts = map (fn (i, (_, _, constrs)) => |
268 val case_fn_Ts = map (fn (i, (_, _, constrs)) => |
269 map (fn (_, cargs) => |
269 map (fn (_, cargs) => |
270 let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs |
270 let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs |
271 in Ts ---> T' end) constrs) (hd descr); |
271 in Ts ---> T' end) constrs) (hd descr); |
308 let |
308 let |
309 val descr' = flat descr; |
309 val descr' = flat descr; |
310 val recTs = Datatype_Aux.get_rec_types descr' sorts; |
310 val recTs = Datatype_Aux.get_rec_types descr' sorts; |
311 val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs; |
311 val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs; |
312 val newTs = take (length (hd descr)) recTs; |
312 val newTs = take (length (hd descr)) recTs; |
313 val T' = TFree (Name.variant used' "'t", HOLogic.typeS); |
313 val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS); |
314 val P = Free ("P", T' --> HOLogic.boolT); |
314 val P = Free ("P", T' --> HOLogic.boolT); |
315 |
315 |
316 fun make_split (((_, (_, _, constrs)), T), comb_t) = |
316 fun make_split (((_, (_, _, constrs)), T), comb_t) = |
317 let |
317 let |
318 val (_, fs) = strip_comb comb_t; |
318 val (_, fs) = strip_comb comb_t; |