--- a/src/ZF/Datatype_ZF.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/Datatype_ZF.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
theory Datatype_ZF
imports Inductive_ZF Univ QUniv
+keywords "datatype" "codatatype" :: thy_decl
uses "Tools/datatype_package.ML"
begin