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_binop2 ctxt s (l, r) = |
|
40 Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) |
|
41 *} |
|
42 |
|
43 ML {* |
|
44 fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv}) |
|
45 fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel}) |
|
46 *} |
38 |
47 |
39 ML {* |
48 ML {* |
40 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees |
49 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees |
41 bn_alphabn alpha_const binds bodys = |
50 bn_alphabn alpha_const binds bodys = |
42 let |
51 let |