--- a/src/HOL/Real/ROOT.ML Tue Oct 26 14:35:45 1999 +0200 +++ b/src/HOL/Real/ROOT.ML Tue Oct 26 15:23:25 1999 +0200 @@ -10,7 +10,6 @@ writeln"Root file for HOL/Real"; -set proof_timing; time_use_thy "RealDef"; use "simproc.ML"; time_use_thy "Real";