equal
deleted
inserted
replaced
207 val lhs = mk_pair (lhs_binds, arg); |
207 val lhs = mk_pair (lhs_binds, arg); |
208 val rhs_binds = fv_binds args2 rbinds; |
208 val rhs_binds = fv_binds args2 rbinds; |
209 val rhs = mk_pair (rhs_binds, arg2); |
209 val rhs = mk_pair (rhs_binds, arg2); |
210 val alpha = nth alpha_frees (body_index dt); |
210 val alpha = nth alpha_frees (body_index dt); |
211 val fv = nth fv_frees (body_index dt); |
211 val fv = nth fv_frees (body_index dt); |
212 val pi = foldr1 add_perm rpis; |
212 val pi = foldr1 add_perm (distinct (op =) rpis); |
213 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
213 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
214 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
214 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
215 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
215 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
216 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
216 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
217 in |
217 in |