1.1 --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sat Nov 21 16:07:58 2009 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sat Nov 21 17:01:44 2009 +0100
     1.3 @@ -98,9 +98,8 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML_type local_theory: Proof.context} \\
     1.6    @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
     1.7 -  @{index_ML Local_Theory.define: "string ->
     1.8 -    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     1.9 -    (term * (string * thm)) * local_theory"} \\
    1.10 +  @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
    1.11 +    local_theory -> (term * (string * thm)) * local_theory"} \\
    1.12    @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
    1.13      local_theory -> (string * thm list) * local_theory"} \\
    1.14    \end{mldecls}
    1.15 @@ -123,7 +122,7 @@
    1.16    --- normally the Isar toplevel already takes care to initialize the
    1.17    local theory context.
    1.18  
    1.19 -  \item @{ML Local_Theory.define}~@{text "kind ((b, mx), (a, rhs))
    1.20 +  \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
    1.21    lthy"} defines a local entity according to the specification that is
    1.22    given relatively to the current @{text "lthy"} context.  In
    1.23    particular the term of the RHS may refer to earlier local entities
    1.24 @@ -143,10 +142,6 @@
    1.25    declarations such as @{attribute simp}, while non-trivial rules like
    1.26    @{attribute simplified} are better avoided.
    1.27  
    1.28 -  The @{text kind} determines the theorem kind tag of the resulting
    1.29 -  fact.  Typical examples are @{ML Thm.definitionK} or @{ML
    1.30 -  Thm.theoremK}.
    1.31 -
    1.32    \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is
    1.33    analogous to @{ML Local_Theory.define}, but defines facts instead of
    1.34    terms.  There is also a slightly more general variant @{ML