--- a/ProgTutorial/FirstSteps.thy	Sat Oct 31 11:37:41 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sun Nov 01 10:49:25 2009 +0100
@@ -132,7 +132,7 @@
 text {*
   During development you might find it necessary to inspect some data in your
   code. This can be done in a ``quick-and-dirty'' fashion using the function
-  @{ML_ind  "writeln"}. For example
+  @{ML_ind writeln in Output}. For example
 
   @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}
 
@@ -140,7 +140,7 @@
   Isabelle.  This function expects a string as argument. If you develop under
   PolyML, then there is a convenient, though again ``quick-and-dirty'', method
   for converting values into strings, namely the function 
-  @{ML_ind  makestring in PolyML}:
+  @{ML_ind makestring in PolyML}:
 
   @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 
 
@@ -150,7 +150,7 @@
   The function @{ML "writeln"} should only be used for testing purposes,
   because any output this function generates will be overwritten as soon as an
   error is raised. For printing anything more serious and elaborate, the
-  function @{ML_ind  tracing} is more appropriate. This function writes all
+  function @{ML_ind tracing in Output} is more appropriate. This function writes all
   output into a separate tracing buffer. For example:
 
   @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
@@ -183,7 +183,7 @@
 
   will cause that all tracing information is printed into the file @{text "foo.bar"}.
 
-  You can print out error messages with the function @{ML_ind  error}; for 
+  You can print out error messages with the function @{ML_ind error in Library}; for 
   example:
 
   @{ML_response_fake [display,gray] 
@@ -195,8 +195,8 @@
   be displayed by the infrastructure.
 
 
-  \footnote{\bf FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 
-  @{ML_ind  profiling in Toplevel}.}
+  \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and 
+  @{ML_ind profiling in Toplevel}.}
 *}
 
 (* FIXME
@@ -234,7 +234,7 @@
 
   We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some
   additional information encoded in it. The string can be properly printed by
-  using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:
+  using either the function @{ML  writeln} or @{ML  tracing}:
 
   @{ML_response_fake [display,gray]
   "writeln (string_of_term @{context} @{term \"1::nat\"})"
@@ -247,7 +247,7 @@
   "\"1\""}
 
   If there are more than one term to be printed, you can use the 
-  function @{ML_ind  commas} to separate them.
+  function @{ML_ind commas in Library} to separate them.
 *} 
 
 ML{*fun string_of_terms ctxt ts =  
@@ -261,9 +261,9 @@
   string_of_term ctxt (term_of ct)*}
 
 text {*
-  In this example the function @{ML_ind term_of} extracts the @{ML_type
+  In this example the function @{ML_ind term_of in Thm} extracts the @{ML_type
   term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
-  printed with @{ML_ind commas}.
+  printed with @{ML commas}.
 *} 
 
 ML{*fun string_of_cterms ctxt cts =  
@@ -271,7 +271,7 @@
 
 text {*
   The easiest way to get the string of a theorem is to transform it
-  into a @{ML_type term} using the function @{ML_ind prop_of}. 
+  into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. 
 *}
 
 ML{*fun string_of_thm ctxt thm =
@@ -340,7 +340,7 @@
 and second half."}
   
   To ease this kind of string manipulations, there are a number
-  of library functions. For example,  the function @{ML_ind  cat_lines}
+  of library functions. For example,  the function @{ML_ind cat_lines in Library}
   concatenates a list of strings and inserts newlines. 
 
   @{ML_response [display, gray]
@@ -715,9 +715,9 @@
   with ML-antiquotations, often just called antiquotations.\footnote{There are
   two kinds of antiquotations in Isabelle, which have very different purposes
   and infrastructures. The first kind, described in this section, are
-  \emph{\index*{ML-antiquotations}}. They are used to refer to entities (like terms,
+  \emph{\index*{ML-antiquotation}}. They are used to refer to entities (like terms,
   types etc) from Isabelle's logic layer inside ML-code. The other kind of
-  antiquotations are \emph{document}\index{document antiquotationa} antiquotations. 
+  antiquotations are \emph{document}\index{document antiquotation} antiquotations. 
   They are used only in the
   text parts of Isabelle and their purpose is to print logical entities inside
   \LaTeX-documents. Document antiquotations are part of the user level and