changeset 12311 | ce5f9e61c037 |
parent 12174 | a0aab0b9f2e9 |
child 12609 | fb073a34b537 |
--- a/src/ZF/Tools/ind_cases.ML Wed Nov 28 00:44:37 2001 +0100 +++ b/src/ZF/Tools/ind_cases.ML Wed Nov 28 00:46:26 2001 +0100 @@ -26,7 +26,6 @@ val empty = Symtab.empty; val copy = I; - val finish = I; val prep_ext = I; fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2); fun print _ _ = ();