--- a/src/Doc/Implementation/Local_Theory.thy Fri Jun 06 12:36:06 2014 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Fri Jun 06 19:19:46 2014 +0200
@@ -96,8 +96,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
- string -> theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\
@{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -120,9 +119,7 @@
non-empty name refers to a @{command locale} or @{command class}
context (a fully-qualified internal name is expected here). This is
useful for experimentation --- normally the Isar toplevel already
- takes care to initialize the local theory context. The given @{text
- "before_exit"} function is invoked before leaving the context; in
- most situations plain identity @{ML I} is sufficient.
+ takes care to initialize the local theory context.
\item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
lthy"} defines a local entity according to the specification that is