changeset 12109 | bd6eb9194a5d |
parent 11938 | 7b594aba1300 |
child 12282 | f98beaaa7c4f |
--- a/src/Provers/simplifier.ML Thu Nov 08 23:57:22 2001 +0100 +++ b/src/Provers/simplifier.ML Thu Nov 08 23:59:37 2001 +0100 @@ -313,6 +313,7 @@ val empty = ref empty_ss; fun copy (ref ss) = (ref ss): T; (*create new reference!*) + val finish = I; val prep_ext = copy; fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); fun print _ (ref ss) = print_ss ss;