diff -r 497e1c9d4a9f -r add17d26151b src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Sep 30 14:32:36 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Sat Sep 30 17:10:55 2006 +0200
@@ -100,6 +100,7 @@
 
 
 lemma Maclaurin_lemma3:
+  fixes difg :: "nat => real => real" shows
      "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
         \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0;  n < m; 0 < t;
         t < h|]