--- a/CookBook/Recipes/Antiquotes.thy	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Sat Nov 29 21:20:18 2008 +0000
@@ -48,7 +48,7 @@
   If the code is ``approved'' by the compiler, then the output function @{ML
   "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the
   code. This function expects that the code is a list of strings where each
-  string correspond to a line (therefore the @{ML_open "(space_explode \"\\n\" txt)" for txt} 
+  string correspond to a line (therefore the @{ML "(space_explode \"\\n\" txt)" for txt} 
   which produces this list).  There are a number of options for antiquotations
   that are observed by @{ML ThyOutput.output_list} when printing the code (for
   example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}).
@@ -146,7 +146,7 @@
 
   In both cases, the check by the compiler ensures that code and result match. A limitation
   of this antiquotation is that the hints can only be given for results that can actually
-  be constructed as a pattern. This excludes values that are abstract types, like 
+  be constructed as a pattern. This excludes values that are abstract datatypes, like 
   theorems or cterms.
 
 *}