src/ZF/Tools/inductive_package.ML

--- a/src/ZF/Tools/inductive_package.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -591,8 +591,9 @@
   >> (Toplevel.theory o mk_ind);
 
 val _ =
-  Outer_Syntax.command (co_prefix ^ "inductive")
-    ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
+  Outer_Syntax.command
+    (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
+    ("define " ^ co_prefix ^ "inductive sets") ind_decl;
 
 end;