--- a/src/HOL/Datatype.thy Thu Oct 04 19:54:44 2007 +0200
+++ b/src/HOL/Datatype.thy Thu Oct 04 19:54:46 2007 +0200
@@ -10,6 +10,7 @@
theory Datatype
imports Finite_Set
+uses "Tools/datatype_codegen.ML"
begin
typedef (Node)
@@ -527,9 +528,6 @@
by auto
-subsection {* Finishing the datatype package setup *}
-
-setup "DatatypeCodegen.setup_hooks"
text {* hides popular names *}
hide (open) type node item
hide (open) const Push Node Atom Leaf Numb Lim Split Case
@@ -685,6 +683,8 @@
subsubsection {* Code generator setup *}
+setup DatatypeCodegen.setup
+
definition
is_none :: "'a option \<Rightarrow> bool" where
is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"