more general type class for factorial. Now allows code generation (?)

--- a/src/HOL/Binomial.thy	Tue Mar 17 14:16:16 2015 +0000
+++ b/src/HOL/Binomial.thy	Tue Mar 17 15:11:25 2015 +0000
@@ -13,7 +13,7 @@
 
 subsection {* Factorial *}
 
-fun fact :: "nat \<Rightarrow> ('a::{semiring_char_0,semiring_no_zero_divisors})"
+fun fact :: "nat \<Rightarrow> ('a::semiring_char_0)"
   where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
 
 lemmas fact_Suc = fact.simps(2)
@@ -30,7 +30,7 @@
 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
   by (cases n) auto
 
-lemma fact_nonzero [simp]: "fact n \<noteq> 0"
+lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
   apply (induct n)
   apply auto
   using of_nat_eq_0_iff by fastforce

--- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 14:16:16 2015 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 15:11:25 2015 +0000
@@ -28,13 +28,6 @@
 
 code_pred sublist .
 
-lemma [code]:  -- {* for the generic factorial function *}
-  fixes XXX :: "'a :: semiring_numeral_div"
-  shows
-   "fact 0       = (1 :: 'a)"
-   "fact (Suc n) = (of_nat (Suc n) * fact n :: 'a)"
- by simp_all
-
 code_reserved SML upto -- {* avoid popular infix *}
 
 end