diff -r a90d0fb24e75 -r 9b6c9d172378 CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Fri Feb 13 01:05:31 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base" Simple_Inductive_Package
 begin
 
-section{* The Interface \label{sec:ind-interface} *}
+section {* The Interface \label{sec:ind-interface} *}
 
 text {*
 
@@ -25,7 +25,7 @@
   invoking the package are reflected in its ML programming interface, which
   consists of two functions:
 
-  @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}
+  @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE}
 *}
 
 text {*