--- a/CookBook/Package/Ind_Code.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -189,6 +189,8 @@
   set up the goals for the induction principles. 
 *}
 
+ML {* singleton *}
+ML {* ProofContext.export *}
 
 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
 let