diff -r bbb2d5f1d58d -r 14c3dd5ee2ad CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Wed Jan 14 18:30:41 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Wed Jan 14 21:46:04 2009 +0000
@@ -301,7 +301,8 @@
 structure of the tokens used, the second part of the library consists of combinators
 for dealing with specific token types.
 The following is an excerpt from the signature of @{ML_struct Scan}:
-\begin{mytable}
+
+\begin{table}
 @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\
 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\
 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\
@@ -311,7 +312,7 @@
 @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\
 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}
-\end{mytable}
+\end{table}
 Interestingly, the functions shown above are so generic that they do not
 even rely on the input and output of the parser being a list of tokens.
 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser
@@ -348,10 +349,12 @@
 from simpler parsers. In order for these combinators to be useful, we also need
 some basic parsers. As an example, we consider the following two parsers
 defined in @{ML_struct Scan}:
-\begin{mytable}
+
+\begin{table}
 @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\
 @{ML "$$ : string -> string list -> string * string list"}
-\end{mytable}
+\end{table}
+
 The parser @{ML "one pred" for pred in Scan} parses exactly one token that
 satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only
 accepts a token that equals the string \texttt{s}. Note that we can easily
@@ -371,7 +374,8 @@
 The parser functions for the theory syntax are contained in the structure
 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
 In our parser, we will use the following functions:
-\begin{mytable}
+
+\begin{table}
 @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\
 @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->
   'a list * token list" in OuterParse} \\
@@ -382,7 +386,8 @@
 @{ML "for_fixes: token list ->
   (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
-\end{mytable}
+\end{table}
+
 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are
 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from
 @{ML_struct Scan}.
@@ -400,10 +405,12 @@
 and @{ML for_fixes in OuterParse}, respectively.
 In addition, the following function from @{ML_struct SpecParse} for parsing
 an optional theorem name and attribute, followed by a delimiter, will be useful:
-\begin{mytable}
+
+\begin{table}
 @{ML "opt_thm_name:
   string -> token list -> Attrib.binding * token list" in SpecParse}
-\end{mytable}
+\end{table}
+
 We now have all the necessary tools to write the parser for our
 \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
 @{ML_chunk [display] syntax}