diff -r 7aa79267fa82 -r 234ef8652cae src/HOL/Power.ML
--- a/src/HOL/Power.ML	Mon Jul 24 23:52:55 2000 +0200
+++ b/src/HOL/Power.ML	Mon Jul 24 23:53:51 2000 +0200
@@ -114,7 +114,7 @@
 
 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
 by (asm_simp_tac
-    (simpset_of Nat.thy addsimps [Suc_times_binomial_eq, 
+    (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
 				  div_mult_self_is_m]) 1);
 qed "binomial_Suc_Suc_eq_times";