--- a/src/HOL/Rat.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Rat.thy Sun Sep 21 16:56:11 2014 +0200
@@ -1151,29 +1151,13 @@
parse_translation {*
let
- fun mk_number i =
- let
- fun mk 1 = Syntax.const @{const_syntax Num.One}
- | mk i =
- let
- val (q, r) = Integer.div_mod i 2;
- val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
- in Syntax.const bit $ (mk q) end;
- in
- if i = 0 then Syntax.const @{const_syntax Groups.zero}
- else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
- else
- Syntax.const @{const_syntax Groups.uminus} $
- (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
- end;
-
fun mk_frac str =
let
val {mant = i, exp = n} = Lexicon.read_float str;
val exp = Syntax.const @{const_syntax Power.power};
- val ten = mk_number 10;
- val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
- in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+ val ten = Numeral.mk_number_syntax 10;
+ val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
+ in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
| float_tr [t as Const (str, _)] = mk_frac str