src/ZF/Tools/induct_tacs.ML
changeset 27353 71c4dd53d4cb
parent 27239 f2f42f9fa09d
child 29579 cb520b766e00
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
     1.8 +val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
     1.9  
    1.10  val rep_datatype_decl =
    1.11    (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --