# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322300894 0
# Node ID 324b148fc6b5985313fea67e632ca28015f28c23
# Parent  41ec301eb062f4b32ff1a373c9d5572fd966e09d
used simproc-antiquotation

diff -r 41ec301eb062 -r 324b148fc6b5 Nominal/nominal_library.ML
--- 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}