src/HOL/Codegenerator_Test/Candidates.thy

--- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Mar 16 15:30:00 2015 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 12:23:56 2015 +0000
@@ -28,6 +28,13 @@
 
 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