diff -r b1a458a03a8e -r 74ba778b09c9 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sat Oct 31 11:37:41 2009 +0100
+++ b/ProgTutorial/General.thy	Sun Nov 01 10:49:25 2009 +0100
@@ -520,7 +520,7 @@
 ML{*fun make_fun_types tys ty = tys ---> ty *}
 
 text {*
-  A handy function for manipulating terms is @{ML_ind  map_types}: it takes a 
+  A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a 
   function and applies it to every type in a term. You can, for example,
   change every @{typ nat} in a term into an @{typ int} using the function:
 *}
@@ -609,7 +609,7 @@
   Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
   enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
-  Given a well-typed term, the function @{ML_ind  type_of} returns the 
+  Given a well-typed term, the function @{ML_ind type_of in Term} returns the 
   type of a term. Consider for example:
 
   @{ML_response [display,gray] 
@@ -624,7 +624,7 @@
   "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
 
   Since the complete traversal might sometimes be too costly and
-  not necessary, there is the function @{ML_ind  fastype_of}, which 
+  not necessary, there is the function @{ML_ind fastype_of in Term}, which 
   also returns the type of a term.
 
   @{ML_response [display,gray] 
@@ -682,7 +682,7 @@
   You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
   typ}es, since they are just arbitrary unchecked trees. However, you
   eventually want to see if a term is well-formed, or type-checks, relative to
-  a theory.  Type-checking is done via the function @{ML_ind  cterm_of}, which
+  a theory.  Type-checking is done via the function @{ML_ind cterm_of in Thm}, which
   converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
   term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
   abstract objects that are guaranteed to be type-correct, and they can only