src/HOL/Tools/numeral_simprocs.ML

--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -169,7 +169,7 @@
 
 fun numtermless tu = (numterm_ord tu = LESS);
 
-val num_ss = HOL_ss settermless numtermless;
+val num_ss = HOL_ss |> Simplifier.set_termless numtermless;
 
 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];