1.1 --- a/src/HOL/Tools/Function/size.ML	Mon Feb 08 17:12:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/size.ML	Mon Feb 08 17:12:27 2010 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  
     1.5      val ctxt = ProofContext.init thy';
     1.6  
     1.7 -    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm add_0_right} ::
     1.8 +    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
     1.9        size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
    1.10      val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
    1.11