# HG changeset patch
# User wenzelm
# Date 979326206 -3600
# Node ID 890b117f61898ad9c44d539cd31cf7477193a64a
# Parent  0b4e916f51ed5ed525523d2c866b6a7e6b368a30
hide dest_bin;

diff -r 0b4e916f51ed -r 890b117f6189 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Fri Jan 12 20:03:04 2001 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Fri Jan 12 20:03:26 2001 +0100
@@ -9,8 +9,7 @@
 
 signature NUMERAL_SYNTAX =
 sig
-  val dest_bin : term -> int
-  val setup    : (theory -> theory) list
+  val setup: (theory -> theory) list
 end;
 
 structure NumeralSyntax: NUMERAL_SYNTAX =