diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Rat.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -6,7 +6,6 @@
 
 theory Rat
 imports GCD Archimedean_Field
-uses ("Tools/float_syntax.ML")
 begin
 
 subsection {* Rational numbers as quotient *}
@@ -1107,7 +1106,7 @@
 
 syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
 
-use "Tools/float_syntax.ML"
+ML_file "Tools/float_syntax.ML"
 setup Float_Syntax.setup
 
 text{* Test: *}