diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Nat.thy	Tue Jan 17 16:36:57 2006 +0100
@@ -1023,5 +1023,12 @@
   apply (fastsimp dest: mult_less_mono2)
   done
 
+subsection {* Code generator setup *}
+
+code_alias
+  "nat" "Nat.nat"
+  "0" "Nat.Zero"
+  "1" "Nat.One"
+  "Suc" "Nat.Suc"
 
 end