equal
deleted
inserted
replaced
175 val descr' = flat descr; |
175 val descr' = flat descr; |
176 val recTs = get_rec_types descr' sorts; |
176 val recTs = get_rec_types descr' sorts; |
177 val used = foldr add_typ_tfree_names (recTs, []); |
177 val used = foldr add_typ_tfree_names (recTs, []); |
178 |
178 |
179 val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~ |
179 val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~ |
180 replicate (length descr') HOLogic.termS); |
180 replicate (length descr') HOLogic.typeS); |
181 |
181 |
182 val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) => |
182 val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) => |
183 map (fn (_, cargs) => |
183 map (fn (_, cargs) => |
184 let |
184 let |
185 val Ts = map (typ_of_dtyp descr' sorts) cargs; |
185 val Ts = map (typ_of_dtyp descr' sorts) cargs; |
239 let |
239 let |
240 val descr' = flat descr; |
240 val descr' = flat descr; |
241 val recTs = get_rec_types descr' sorts; |
241 val recTs = get_rec_types descr' sorts; |
242 val used = foldr add_typ_tfree_names (recTs, []); |
242 val used = foldr add_typ_tfree_names (recTs, []); |
243 val newTs = take (length (hd descr), recTs); |
243 val newTs = take (length (hd descr), recTs); |
244 val T' = TFree (variant used "'t", HOLogic.termS); |
244 val T' = TFree (variant used "'t", HOLogic.typeS); |
245 |
245 |
246 val case_fn_Ts = map (fn (i, (_, _, constrs)) => |
246 val case_fn_Ts = map (fn (i, (_, _, constrs)) => |
247 map (fn (_, cargs) => |
247 map (fn (_, cargs) => |
248 let val Ts = map (typ_of_dtyp descr' sorts) cargs |
248 let val Ts = map (typ_of_dtyp descr' sorts) cargs |
249 in Ts ---> T' end) constrs) (hd descr); |
249 in Ts ---> T' end) constrs) (hd descr); |
324 let |
324 let |
325 val descr' = flat descr; |
325 val descr' = flat descr; |
326 val recTs = get_rec_types descr' sorts; |
326 val recTs = get_rec_types descr' sorts; |
327 val used' = foldr add_typ_tfree_names (recTs, []); |
327 val used' = foldr add_typ_tfree_names (recTs, []); |
328 val newTs = take (length (hd descr), recTs); |
328 val newTs = take (length (hd descr), recTs); |
329 val T' = TFree (variant used' "'t", HOLogic.termS); |
329 val T' = TFree (variant used' "'t", HOLogic.typeS); |
330 val P = Free ("P", T' --> HOLogic.boolT); |
330 val P = Free ("P", T' --> HOLogic.boolT); |
331 |
331 |
332 fun make_split (((_, (_, _, constrs)), T), comb_t) = |
332 fun make_split (((_, (_, _, constrs)), T), comb_t) = |
333 let |
333 let |
334 val (_, fs) = strip_comb comb_t; |
334 val (_, fs) = strip_comb comb_t; |