src/HOL/ex/Classpackage.thy

--- a/src/HOL/ex/Classpackage.thy	Thu Oct 04 19:42:03 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy	Thu Oct 04 19:46:09 2007 +0200
@@ -293,6 +293,8 @@
 end
 
 (*FIXME*)
+thm (no_abbrevs) pow_def
+thm (no_abbrevs) pow_def [folded monoid_class.npow]
 lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
 
 context group begin