equal
deleted
inserted
replaced
339 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
339 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
340 val ty = fastype_of (bn $ arg) |
340 val ty = fastype_of (bn $ arg) |
341 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
341 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
342 in |
342 in |
343 if bns_same rel_in_comp_binds then |
343 if bns_same rel_in_comp_binds then |
344 HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) |
344 alpha_bn |
|
345 (* HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))*) |
345 else error "incompatible bindings for one argument" |
346 else error "incompatible bindings for one argument" |
346 end |
347 end |
347 | ([], [], relevant) => |
348 | ([], [], relevant) => |
348 let |
349 let |
349 val (rbinds, rpis) = split_list relevant |
350 val (rbinds, rpis) = split_list relevant |