equal
deleted
inserted
replaced
85 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs |
85 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs |
86 val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) |
86 val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) |
87 val t = Syntax.check_term lthy alpha_gen_ex |
87 val t = Syntax.check_term lthy alpha_gen_ex |
88 in |
88 in |
89 case binds of |
89 case binds of |
90 [(SOME bn, i)] => if i mem bodys then [t] |
90 [(SOME bn, i)] => if member (op =) bodys i then [t] |
91 else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)] |
91 else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)] |
92 | _ => [t] |
92 | _ => [t] |
93 end |
93 end |
94 *} |
94 *} |
95 |
95 |