diff -r 509b1da3cee1 -r 2284e0d02e7f src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Mon May 14 12:52:54 2007 +0200
+++ b/src/HOL/Real/Float.thy	Mon May 14 12:52:56 2007 +0200
@@ -7,7 +7,7 @@
 
 theory Float
 imports Real Parity
-uses ("float.ML")
+uses "~~/src/Pure/General/float.ML" ("float_arith.ML")
 begin
 
 definition
@@ -526,6 +526,6 @@
 (* for use with the compute oracle *)
 lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
 
-use "float.ML";
+use "float_arith.ML";
 
 end