# HG changeset patch
# User blanchet
# Date 1392190648 -3600
# Node ID 07dea66779f33be28eef59c7a3bcfc08eefe49de
# Parent  6445a05a123493740c199ab53e773146c1372d18
for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'

diff -r 6445a05a1234 -r 07dea66779f3 src/HOL/Nat.thy
--- 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 *}