# HG changeset patch
# User haftmann
# Date 1159822874 -7200
# Node ID 7e8c724339e0a9c269e49981bfcd463baab9ba5e
# Parent  5fde744176d744392637f042d132bb8702dd030a
clarified setup name

diff -r 5fde744176d7 -r 7e8c724339e0 src/HOL/Datatype.thy
--- 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