--- 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.