src/HOL/Hyperreal/Fact.thy

--- a/src/HOL/Hyperreal/Fact.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -54,7 +54,7 @@
 
 lemma fact_diff_Suc [rule_format]:
     "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-  apply (induct n fixing: m)
+  apply (induct n arbitrary: m)
   apply auto
   apply (drule_tac x = "m - 1" in meta_spec, auto)
   done