no_notation instead of hide;

--- a/src/HOL/Algebra/AbelCoset.thy	Fri Jun 13 21:04:07 2008 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Fri Jun 13 21:04:09 2008 +0200
@@ -16,7 +16,7 @@
 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
   up with better syntax here *}
 
-hide const Plus
+no_notation Plus (infixr "<+>" 65)
 
 constdefs (structure G)
   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)