for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'

--- a/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
@@ -132,7 +132,7 @@
 lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
   -- {* for backward compatibility -- names of variables differ *}
   "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
-by (rule nat.exhaust)
+by (rule old.nat.exhaust)
 
 lemma nat_induct [case_names 0 Suc, induct type: nat]:
   -- {* for backward compatibility -- names of variables differ *}