src/HOL/Tools/numeral_syntax.ML

       | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
   in mk (#value (Lexicon.read_xnum num)) end;
 
 in
 
-fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
-      Syntax.const @{const_syntax Int.number_of} $ mk_bin num
-  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
+fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u
+  | numeral_tr [t as Const (num, _)] = Syntax.const @{const_syntax Int.number_of} $ mk_bin num
+  | numeral_tr ts = raise TERM ("numeral_tr", ts);
 
 end;
 
 
 (* print translation *)