equal
deleted
inserted
replaced
86 |
86 |
87 |
87 |
88 (* local assumptions *) |
88 (* local assumptions *) |
89 |
89 |
90 fun local_assumptions_of inner outer = |
90 fun local_assumptions_of inner outer = |
91 Library.drop (length (all_assumptions_of outer), all_assumptions_of inner); |
91 (uncurry drop) (length (all_assumptions_of outer), all_assumptions_of inner); |
92 |
92 |
93 val local_assms_of = maps #2 oo local_assumptions_of; |
93 val local_assms_of = maps #2 oo local_assumptions_of; |
94 |
94 |
95 fun local_prems_of inner outer = |
95 fun local_prems_of inner outer = |
96 Library.drop (length (all_prems_of outer), all_prems_of inner); |
96 (uncurry drop) (length (all_prems_of outer), all_prems_of inner); |
97 |
97 |
98 |
98 |
99 (* add assumptions *) |
99 (* add assumptions *) |
100 |
100 |
101 fun add_assms export new_asms = |
101 fun add_assms export new_asms = |