src/HOL/Metis_Examples/Type_Encodings.thy

--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Nov 15 09:22:19 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Nov 15 12:39:29 2011 +0100
@@ -107,6 +107,6 @@
 by (metis_exhaust null_def)
 
 lemma "(0::nat) + 0 = 0"
-by (metis_exhaust arithmetic_simps(38))
+by (metis_exhaust add_0_left)
 
 end