diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Tools/float_syntax.ML	Thu Feb 11 23:00:22 2010 +0100
@@ -1,7 +1,6 @@
-(*  ID:         $Id$
-    Authors:    Tobias Nipkow, TU Muenchen
+(*  Author:     Tobias Nipkow, TU Muenchen
 
-Concrete syntax for floats
+Concrete syntax for floats.
 *)
 
 signature FLOAT_SYNTAX =
@@ -18,19 +17,21 @@
 
 fun mk_number i =
   let
-    fun mk 0 = Syntax.const @{const_name Int.Pls}
-      | mk ~1 =  Syntax.const @{const_name Int.Min}
-      | mk i = let val (q, r) = Integer.div_mod i 2
-               in HOLogic.mk_bit r $ (mk q) end;
-  in Syntax.const @{const_name Int.number_of} $ mk i end;
+    fun mk 0 = Syntax.const @{const_syntax Int.Pls}
+      | mk ~1 = Syntax.const @{const_syntax Int.Min}
+      | mk i =
+          let val (q, r) = Integer.div_mod i 2
+          in HOLogic.mk_bit r $ (mk q) end;
+  in Syntax.const @{const_syntax Int.number_of} $ mk i end;
 
 fun mk_frac str =
   let
-    val {mant=i, exp = n} = Syntax.read_float str;
-    val exp = Syntax.const @{const_name Power.power};
+    val {mant = i, exp = n} = Syntax.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_name divide}) $ (mk_number i) $ exp10 end
+    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
+  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+
 in
 
 fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
@@ -42,6 +43,6 @@
 (* theory setup *)
 
 val setup =
-  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
+  Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
 
 end;