changeset 74561 | 8e6c973003c8 |
parent 74302 | 6bc96f31cafd |
--- a/src/Sequents/prover.ML Wed Oct 20 17:11:46 2021 +0200 +++ b/src/Sequents/prover.ML Wed Oct 20 18:13:17 2021 +0200 @@ -46,7 +46,6 @@ ( type T = pack; val empty = empty_pack; - val extend = I; fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) = Pack (sort_rules (Thm.merge_thms (safes, safes')),