equal
deleted
inserted
replaced
86 fun mk_alpha_term bmode fv alpha args args' binders binders' = |
86 fun mk_alpha_term bmode fv alpha args args' binders binders' = |
87 let |
87 let |
88 val (alpha_name, binder_ty) = |
88 val (alpha_name, binder_ty) = |
89 case bmode of |
89 case bmode of |
90 Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) |
90 Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) |
91 | Set => (@{const_name "alpha_gen"}, @{typ "atom set"}) |
91 | Set => (@{const_name "alpha_set"}, @{typ "atom set"}) |
92 | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) |
92 | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) |
93 val ty = fastype_of args |
93 val ty = fastype_of args |
94 val pair_ty = HOLogic.mk_prodT (binder_ty, ty) |
94 val pair_ty = HOLogic.mk_prodT (binder_ty, ty) |
95 val alpha_ty = [ty, ty] ---> @{typ "bool"} |
95 val alpha_ty = [ty, ty] ---> @{typ "bool"} |
96 val fv_ty = ty --> @{typ "atom set"} |
96 val fv_ty = ty --> @{typ "atom set"} |