diff -r b4234e8a0202 -r 12533bb49615 CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Thu Feb 12 14:15:50 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Thu Feb 12 16:09:42 2009 +0000
@@ -14,9 +14,4 @@
 
 *}
 
-text {*
-
-  @{ML_chunk [display,gray] storing}
-
-*}
 end