src/HOL/Real/ROOT.ML

--- a/src/HOL/Real/ROOT.ML	Tue Aug 24 11:50:58 1999 +0200
+++ b/src/HOL/Real/ROOT.ML	Tue Aug 24 11:54:13 1999 +0200
@@ -11,6 +11,6 @@
 set proof_timing;
 time_use_thy "RealDef";
 use          "simproc.ML";
-time_use_thy "RComplete";
+time_use_thy "Real";
 time_use_thy "Hyperreal/Filter";
 time_use_thy "Hyperreal/HyperDef";