diff -r 7860ffc5ec08 -r 287182c2f23a doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Mon Jun 06 18:05:38 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Jun 06 19:08:46 2011 +0200
@@ -366,6 +366,7 @@
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
+  @{index_ML incr_boundvars: "int -> term -> term"} \\
   @{index_ML Sign.declare_const: "Proof.context ->
   (binding * typ) * mixfix -> theory -> term * theory"} \\
   @{index_ML Sign.add_abbrev: "string -> binding * term ->
@@ -414,6 +415,12 @@
   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   abstraction.
 
+  \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling
+  bound variables by the offset @{text "j"}.  This is required when
+  moving a subterm into a context where it is enclosed by a different
+  number of abstractions.  Bound variables with a matching abstraction
+  are unaffected.
+
   \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
   a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.