diff -r aed0a0450797 -r 0b4e916f51ed src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Fri Jan 12 18:00:40 2001 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Fri Jan 12 20:03:04 2001 +0100
@@ -83,8 +83,8 @@
 
 (*Decodes a binary INTEGER*)
 fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
-     (NumeralSyntax.dest_bin w
-      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+     (HOLogic.dest_binum w
+      handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =