# HG changeset patch
# User wenzelm
# Date 1170359990 -3600
# Node ID 8e127313ed55c0152bcff0bb105608c8b77cf735
# Parent  7c27195a4afc6e1219780af1e96175fd402f1b7c
tuned;

diff -r 7c27195a4afc -r 8e127313ed55 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu Feb 01 20:40:34 2007 +0100
+++ b/src/HOL/ex/Binary.thy	Thu Feb 01 20:59:50 2007 +0100
@@ -195,7 +195,7 @@
 
 val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
 
-fun binary_tr [t as Const (num, _)] =
+fun binary_tr [Const (num, _)] =
       let
         val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
         val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);