src/ZF/Tools/inductive_package.ML

   end;
 
 
 (* outer syntax *)
 
-val _ = List.app Keyword.keyword
-  ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
-
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
 
 val ind_decl =
   (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --