diff -r 08d227db6c74 -r 503ac4c5ef91 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