--- a/Nominal/nominal_library.ML	Sat Nov 26 09:47:21 2011 +0000
+++ b/Nominal/nominal_library.ML	Sat Nov 26 09:48:14 2011 +0000
@@ -346,7 +346,7 @@
 
 (* simpset for size goals *)
 val size_simpset = HOL_ss
-   addsimprocs Nat_Numeral_Simprocs.cancel_numerals
+   addsimprocs [@{simproc natless_cancel_numerals}]
    addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
      zero_less_Suc prod.size(1) mult_Suc_right}