changeset 12109 | bd6eb9194a5d |
parent 12053 | 7e2e84e503ce |
child 12311 | ce5f9e61c037 |
--- a/src/Provers/classical.ML Thu Nov 08 23:57:22 2001 +0100 +++ b/src/Provers/classical.ML Thu Nov 08 23:59:37 2001 +0100 @@ -922,6 +922,7 @@ val empty = ref empty_cs; fun copy (ref cs) = (ref cs): T; (*create new reference!*) + val finish = I; val prep_ext = copy; fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); fun print _ (ref cs) = print_cs cs;