src/ZF/Tools/induct_tacs.ML

--- a/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -188,7 +188,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
+val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
 
 val rep_datatype_decl =
   (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --