tuned;

--- a/src/HOL/Real/Float.ML	Thu Jul 14 17:16:52 2005 +0200
+++ b/src/HOL/Real/Float.ML	Thu Jul 14 17:21:35 2005 +0200
@@ -17,11 +17,6 @@
 =
 struct
 
-fun fst (a,b) = a
-fun snd (a,b) = b
-
-val filter = List.filter;
-
 exception Destruct_floatstr of string;
 
 fun destruct_floatstr isDigit isExp number = 

--- a/src/HOL/Real/ROOT.ML	Thu Jul 14 17:16:52 2005 +0200
+++ b/src/HOL/Real/ROOT.ML	Thu Jul 14 17:21:35 2005 +0200
@@ -7,5 +7,4 @@
 by Jacques Fleuriot
 *)
 
-time_use_thy "Real";
-use_thy "Float";
\ No newline at end of file
+time_use_thy "Float";