src/HOL/Tools/float_syntax.ML
changeset 32603 e08fdd615333
parent 28952 15a4b2cf8c34
child 35115 446c5063e4fd
     1.1 --- a/src/HOL/Tools/float_syntax.ML	Fri Sep 18 09:07:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/float_syntax.ML	Fri Sep 18 09:07:50 2009 +0200
     1.3 @@ -27,10 +27,10 @@
     1.4  fun mk_frac str =
     1.5    let
     1.6      val {mant=i, exp = n} = Syntax.read_float str;
     1.7 -    val exp = Syntax.const @{const_name "Power.power"};
     1.8 +    val exp = Syntax.const @{const_name Power.power};
     1.9      val ten = mk_number 10;
    1.10      val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
    1.11 -  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
    1.12 +  in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
    1.13  in
    1.14  
    1.15  fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str