diff -r 748d9c1a32fb -r fcc0e6e54dca CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -245,15 +245,6 @@
   predicates, the names and types of their parameters, the actual introduction
   rules and a \emph{local theory}.  They return a local theory containing the
   definition and the induction principle as well introduction rules. 
-  
-  In contrast to an ordinary theory, which simply consists of a type
-  signature, as well as tables for constants, axioms and theorems, a local
-  theory also contains additional context information, such as locally fixed
-  variables and local assumptions that may be used by the package. The type
-  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
-  @{ML_type "Proof.context"}, although not every proof context constitutes a
-  valid local theory.
-
 
   Note that @{ML add_inductive_i in SimpleInductivePackage} expects
   the types of the predicates and parameters to be specified using the