| changeset 12311 | ce5f9e61c037 |
| parent 12204 | 98115606ee42 |
| child 14153 | 76a6ba67bd15 |
--- a/src/ZF/Tools/induct_tacs.ML Wed Nov 28 00:44:37 2001 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Wed Nov 28 00:46:26 2001 +0100 @@ -37,7 +37,6 @@ val empty = Symtab.empty; val copy = I; - val finish = I; val prep_ext = I; val merge: T * T -> T = Symtab.merge (K true); @@ -65,7 +64,6 @@ val empty = Symtab.empty val copy = I; - val finish = I; val prep_ext = I val merge: T * T -> T = Symtab.merge (K true)