removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;

--- a/src/HOL/Real/RealVector.thy	Sat Sep 01 15:47:05 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Sat Sep 01 16:12:50 2007 +0200
@@ -376,11 +376,10 @@
 
 instance real :: norm
   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
-ML"set Toplevel.debug"
 
 class sgn_div_norm = scaleR + inverse + norm + sgn +
 assumes sgn_div_norm: "sgn x = x /# norm x"
-(* FIXME junk needed because of bug in locales *)
+(* FIXME junk needed because of broken locale interpretation *)
 and "(sgn :: 'a::scaleR \<Rightarrow> 'a) = sgn"
 and "(inverse :: 'a::scaleR \<Rightarrow> 'a) = inverse"
 and "(scaleR :: real \<Rightarrow> 'a::scaleR \<Rightarrow> 'a) = scaleR"