# HG changeset patch
# User wenzelm
# Date 1188655970 -7200
# Node ID f39e79334052442caae815d710aae5654fc21faa
# Parent  fc4959967b3041925be389ce6c8c54400bfb8ece
removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;

diff -r fc4959967b30 -r f39e79334052 src/HOL/Real/RealVector.thy
--- 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"