equal
deleted
inserted
replaced
33 in |
33 in |
34 fold fold_fun tys (Abs ("", tyh, abs_rhs)) |
34 fold fold_fun tys (Abs ("", tyh, abs_rhs)) |
35 end; |
35 end; |
36 *} |
36 *} |
37 |
37 |
38 ML {* |
|
39 fun mk_pair (fst, snd) = |
|
40 let |
|
41 val ty1 = fastype_of fst |
|
42 val ty2 = fastype_of snd |
|
43 val c = HOLogic.pair_const ty1 ty2 |
|
44 in |
|
45 c $ fst $ snd |
|
46 end; |
|
47 *} |
|
48 |
38 |
49 ML {* |
39 ML {* |
50 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees |
40 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees |
51 bn_alphabn alpha_const binds bodys = |
41 bn_alphabn alpha_const binds bodys = |
52 let |
42 let |
63 else mk_union (map (bind_set args) nos); |
53 else mk_union (map (bind_set args) nos); |
64 val lhs_binds = binds_fn args binds; |
54 val lhs_binds = binds_fn args binds; |
65 val rhs_binds = binds_fn args2 binds; |
55 val rhs_binds = binds_fn args2 binds; |
66 val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys); |
56 val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys); |
67 val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys); |
57 val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys); |
68 val lhs = mk_pair (lhs_binds, lhs_bodys); |
58 val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys); |
69 val rhs = mk_pair (rhs_binds, rhs_bodys); |
59 val rhs = HOLogic.mk_prod (rhs_binds, rhs_bodys); |
70 val body_dts = map (nth dts) bodys; |
60 val body_dts = map (nth dts) bodys; |
71 fun fv_for_dt dt = |
61 fun fv_for_dt dt = |
72 if Datatype_Aux.is_rec_type dt |
62 if Datatype_Aux.is_rec_type dt |
73 then nth fv_frees (Datatype_Aux.body_index dt) |
63 then nth fv_frees (Datatype_Aux.body_index dt) |
74 else Const (@{const_name supp}, |
64 else Const (@{const_name supp}, |