src/HOL/ex/Binary.thy
changeset 22229 8e127313ed55
parent 22205 23bd1ed32ac0
child 22997 d4f3b015b50b
equal deleted inserted replaced
22228:7c27195a4afc 22229:8e127313ed55
   193 parse_translation {*
   193 parse_translation {*
   194 let
   194 let
   195 
   195 
   196 val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
   196 val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
   197 
   197 
   198 fun binary_tr [t as Const (num, _)] =
   198 fun binary_tr [Const (num, _)] =
   199       let
   199       let
   200         val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
   200         val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
   201         val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   201         val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   202       in syntax_consts (mk_binary n) end
   202       in syntax_consts (mk_binary n) end
   203   | binary_tr ts = raise TERM ("binary_tr", ts);
   203   | binary_tr ts = raise TERM ("binary_tr", ts);