--- a/src/ZF/Tools/numeral_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -71,7 +71,7 @@
(* translation of integer constant tokens to and from binary *)
fun int_tr [t as Free (str, _)] =
- Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
+ Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str))
| int_tr ts = raise TERM ("int_tr", ts);
fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)