diff -r 4e2341f6599d -r fb8f22dd8ad0 CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy	Mon Mar 16 00:12:32 2009 +0100
@@ -360,6 +360,8 @@
   The definition of the transitive closure should look as follows:
 *}
 
+ML {* SpecParse.opt_thm_name *}
+
 text {*
 
   A proposition can be parsed using the function @{ML prop in OuterParse}.
@@ -377,7 +379,7 @@
   
   \begin{table}
   @{ML "opt_thm_name:
-  string -> token list -> Attrib.binding * token list" in SpecParse}
+  string -> Attrib.binding parser" in SpecParse}
   \end{table}
 
   We now have all the necessary tools to write the parser for our