diff -r b5914f3c643c -r 5b9c6010897b CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -434,14 +434,21 @@
   (local_theory -> local_theory) ->
   Toplevel.transition -> Toplevel.transition"}
 which, apart from the local theory transformer, takes an optional name of a locale
-to be used as a basis for the local theory. The whole parser for our command has type
-@{ML_type [display] "OuterLex.token list ->
+to be used as a basis for the local theory. 
+
+(FIXME : needs to be adjusted to new parser type)
+
+{\it
+The whole parser for our command has type
+@{ML_text [display] "OuterLex.token list ->
   (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"}
-which is abbreviated by @{ML_type OuterSyntax.parser_fn}. The new command can be added
+which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added
 to the system via the function
-@{ML [display] "OuterSyntax.command :
+@{ML_text [display] "OuterSyntax.command :
   string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"}
-which imperatively updates the parser table behind the scenes. In addition to the parser, this
+which imperatively updates the parser table behind the scenes. }
+
+In addition to the parser, this
 function takes two strings representing the name of the command and a short description,
 as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of
 command we intend to add. Since we want to add a command for declaring new concepts,