diff -r 893062359bec -r 1bdef0c013d3 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Feb 09 11:47:47 2010 +0100
@@ -153,7 +153,7 @@
 
     val ctxt = ProofContext.init thy';
 
-    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
+    val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
       size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
     val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);