diff -r 0cca8d19557d -r 42ee69856dd0 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Nov 06 16:28:36 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Nov 06 16:28:37 2006 +0100
@@ -591,11 +591,11 @@
 structure Type = ROOT.Type;
 structure Lambda = ROOT.Lambda;
 
-fun nat_of_int 0 = ROOT.IntDef.Zero_nat
-  | nat_of_int n = ROOT.IntDef.Succ_nat (nat_of_int (n-1));
+fun nat_of_int 0 = ROOT.Nat.Zero_nat
+  | nat_of_int n = ROOT.Nat.Suc (nat_of_int (n-1));
 
-fun int_of_nat ROOT.IntDef.Zero_nat = 0
-  | int_of_nat (ROOT.IntDef.Succ_nat n) = 1 + int_of_nat n;
+fun int_of_nat ROOT.Nat.Zero_nat = 0
+  | int_of_nat (ROOT.Nat.Suc n) = 1 + int_of_nat n;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
@@ -632,7 +632,7 @@
       let val dBT = dBtype_of_typ T
       in Norm.Abs_1 (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
-        typing_of_term (T :: Ts) (Type.shift e ROOT.IntDef.Zero_nat dBT) t)
+        typing_of_term (T :: Ts) (Type.shift e ROOT.Nat.Zero_nat dBT) t)
       end
   | typing_of_term _ _ _ = error "typing_of_term: bad term";