# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493218636 -3600
# Node ID 1d9a96750a409ecc2160be1b9691c201e191328d
# Parent  8d53b3bebab4a5061c2db33fb2b154522c280e0b# Parent  baf96277ee7624fa5f0e739dadc9600731469dab
Merge

diff -r 8d53b3bebab4 -r 1d9a96750a40 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Apr 26 15:53:35 2017 +0100
+++ b/src/HOL/Binomial.thy	Wed Apr 26 15:57:16 2017 +0100
@@ -1688,10 +1688,8 @@
     (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric]
       atLeastLessThanSuc_atLeastAtMost)
 
-(* FIXME *)
-(*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
-
-(*
+lemmas [code del] = binomial_Suc_Suc binomial_n_0 binomial_0_Suc
+    
 lemma binomial_code [code]:
   "(n choose k) =
       (if k > n then 0
@@ -1702,10 +1700,9 @@
     assume "k \<le> n"
     then have "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
     then have "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"
-      by (simp add: prod.union_disjoint fact_altdef_nat)
+      by (simp add: prod.union_disjoint fact_prod)
   }
   then show ?thesis by (auto simp: binomial_altdef_nat mult_ac prod_atLeastAtMost_code)
 qed
-*)
 
 end