src/HOL/Code_Numeral.thy
changeset 55642 63beb38e9258
parent 55428 0ab52bf7b5e6
child 55736 f1ed1e9cd080
--- a/src/HOL/Code_Numeral.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -888,7 +888,7 @@
   "case_natural f g n = (if n = 0 then f else g (n - 1))"
   by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
 
-declare natural.recs [code del]
+declare natural.rec [code del]
 
 lemma [code abstract]:
   "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"