--- a/src/ZF/Tools/induct_tacs.ML Wed Apr 13 18:45:09 2005 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Wed Apr 13 18:45:25 2005 +0200 @@ -232,3 +232,4 @@ val exhaust_tac = DatatypeTactics.exhaust_tac; val induct_tac = DatatypeTactics.induct_tac; +