src/ZF/Tools/induct_tacs.ML

 
 
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
+  Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
     ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
      (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
      (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
      Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.xthms1) []
      >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));