changeset 12311 | ce5f9e61c037 |
parent 12123 | 739eba13e2cd |
child 13105 | 3d1e7a199bdc |
--- a/src/Sequents/prover.ML Wed Nov 28 00:44:37 2001 +0100 +++ b/src/Sequents/prover.ML Wed Nov 28 00:46:26 2001 +0100 @@ -174,7 +174,6 @@ type T = pack ref; val empty = ref empty_pack fun copy (ref pack) = ref pack; - val finish = I; val prep_ext = copy; fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2)); fun print _ (ref pack) = print_pack pack;