diff -r efc5f4806cd5 -r c141f139ce26 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/MacLaurin.thy	Fri Jul 17 13:12:18 2009 -0400
@@ -58,17 +58,17 @@
  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
  apply (simp del: setsum_op_ivl_Suc)
  apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
+ apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
    apply (rule_tac [2] DERIV_const)
   apply (rule DERIV_sumr, clarify)
   prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
+ apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
   apply (best intro!: DERIV_intros)
- apply (subst fact_Suc_nat)
+ apply (subst fact_Suc)
  apply (subst real_of_nat_mult)
  apply (simp add: mult_ac)
 done
@@ -120,7 +120,7 @@
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
     apply (insert sumr_offset4 [of "Suc 0"])
-    apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
+    apply (simp del: setsum_op_ivl_Suc fact_Suc)
     done
 
   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
@@ -180,7 +180,7 @@
       (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
       diff n t / real (fact n) * h ^ n"
       using `difg (Suc m) t = 0`
-      by (simp add: m f_h difg_def del: fact_Suc_nat)
+      by (simp add: m f_h difg_def del: fact_Suc)
   qed
 
 qed