diff -r 179ff9cb160b -r 5b25fee0362c src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Fact.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -7,7 +7,7 @@
 header{*Factorial Function*}
 
 theory Fact
-imports Nat
+imports Main
 begin
 
 consts fact :: "nat => nat"
@@ -58,7 +58,7 @@
   "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
 apply (induct n arbitrary: m)
 apply auto
-apply (drule_tac x = "m - 1" in meta_spec, auto)
+apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
 done
 
 lemma fact_num0: "fact 0 = 1"