src/HOL/Tools/inductive_set.ML

 (* commands *)
 
 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
+  Outer_Syntax.local_theory @{command_keyword inductive_set} "define inductive sets"
     (ind_set_decl false);
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
+  Outer_Syntax.local_theory @{command_keyword coinductive_set} "define coinductive sets"
     (ind_set_decl true);
 
 end;