--- a/src/HOL/Import/HOL/num.imp	Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/num.imp	Wed Sep 07 07:59:45 2011 +0900
@@ -7,12 +7,12 @@
 
 const_maps
   "SUC" > "Nat.Suc"
-  "0" > "0" :: "nat"
+  "0" > "Groups.zero_class.zero" :: "nat"
 
 thm_maps
-  "NOT_SUC" > "Nat.nat.simps_1"
+  "NOT_SUC" > "Nat.Suc_not_Zero"
   "INV_SUC" > "Nat.Suc_inject"
-  "INDUCTION" > "List.lexn.induct"
+  "INDUCTION" > "Fact.fact_nat.induct"
 
 ignore_thms
   "num_TY_DEF"