--- a/src/HOL/Datatype.thy Mon Oct 02 23:01:11 2006 +0200
+++ b/src/HOL/Datatype.thy Mon Oct 02 23:01:14 2006 +0200
@@ -12,7 +12,6 @@
imports NatArith Sum_Type
begin
-
typedef (Node)
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
--{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
@@ -537,14 +536,13 @@
subsection {* Finishing the datatype package setup *}
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
+setup "DatatypeCodegen.setup_hooks"
hide (open) const Push Node Atom Leaf Numb Lim Split Case
hide (open) type node item
section {* Datatypes *}
-setup "DatatypeCodegen.setup2"
-
subsection {* Representing primitive types *}
rep_datatype bool