src/HOL/ex/Birthday_Paradox.thy

--- a/src/HOL/ex/Birthday_Paradox.thy	Tue Mar 10 16:12:35 2015 +0000
+++ b/src/HOL/ex/Birthday_Paradox.thy	Mon Mar 16 15:30:00 2015 +0000
@@ -51,7 +51,7 @@
     using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
     by (simp add: fact_mod)
   also have "... = fact (card T) div fact (card T - card (insert x S))"
-    using insert by (simp add: fact_reduce_nat[of "card T"])
+    using insert by (simp add: fact_reduce[of "card T"])
   finally show ?case .
 qed