--- a/CookBook/Package/Ind_Interface.thy	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sat Feb 07 12:05:02 2009 +0000
@@ -250,11 +250,6 @@
 thm rel.accpartI'
 thm rel.accpart'.induct
 
-ML{*val (result, lthy) = SimpleInductivePackage.add_inductive
-  [(Binding.name "trcl'", NONE, NoSyn)] [(Binding.name "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)]
-  [((Binding.name "base", []), "\<And>x. trcl' r x x"), ((Binding.name "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")]
-  (TheoryTarget.init NONE @{theory})
-*}
 (*>*)
 
 text {*
@@ -460,11 +455,11 @@
 
   {\it
   The whole parser for our command has type
-  @{ML_text [display] "OuterLex.token list ->
+  @{text [display] "OuterLex.token list ->
   (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"}
-  which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added
+  which is abbreviated by @{text OuterSyntax.parser_fn}. The new command can be added
   to the system via the function
-  @{ML_text [display] "OuterSyntax.command :
+  @{text [display] "OuterSyntax.command :
   string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"}
   which imperatively updates the parser table behind the scenes. }