adapted local theory operations -- eliminated odd kind;

--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sat Nov 21 16:07:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sat Nov 21 17:01:44 2009 +0100
@@ -98,9 +98,8 @@
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
   @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
-  @{index_ML Local_Theory.define: "string ->
-    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
-    (term * (string * thm)) * local_theory"} \\
+  @{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 ->
     local_theory -> (string * thm list) * local_theory"} \\
   \end{mldecls}
@@ -123,7 +122,7 @@
   --- normally the Isar toplevel already takes care to initialize the
   local theory context.
 
-  \item @{ML Local_Theory.define}~@{text "kind ((b, mx), (a, rhs))
+  \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
   lthy"} defines a local entity according to the specification that is
   given relatively to the current @{text "lthy"} context.  In
   particular the term of the RHS may refer to earlier local entities
@@ -143,10 +142,6 @@
   declarations such as @{attribute simp}, while non-trivial rules like
   @{attribute simplified} are better avoided.
 
-  The @{text kind} determines the theorem kind tag of the resulting
-  fact.  Typical examples are @{ML Thm.definitionK} or @{ML
-  Thm.theoremK}.
-
   \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is
   analogous to @{ML Local_Theory.define}, but defines facts instead of
   terms.  There is also a slightly more general variant @{ML

--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Sat Nov 21 16:07:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Sat Nov 21 17:01:44 2009 +0100
@@ -124,9 +124,8 @@
 \begin{mldecls}
   \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
   \indexdef{}{ML}{Theory\_Target.init}\verb|Theory_Target.init: string option -> theory -> local_theory| \\[1ex]
-  \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: string ->|\isasep\isanewline%
-\verb|    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->|\isasep\isanewline%
-\verb|    (term * (string * thm)) * local_theory| \\
+  \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
+\verb|    local_theory -> (term * (string * thm)) * local_theory| \\
   \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
 \verb|    local_theory -> (string * thm list) * local_theory| \\
   \end{mldecls}
@@ -148,7 +147,7 @@
   --- normally the Isar toplevel already takes care to initialize the
   local theory context.
 
-  \item \verb|Local_Theory.define|~\isa{kind\ {\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
+  \item \verb|Local_Theory.define|~\isa{{\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
   given relatively to the current \isa{lthy} context.  In
   particular the term of the RHS may refer to earlier local entities
   from the auxiliary context, or hypothetical parameters from the
@@ -167,9 +166,6 @@
   declarations such as \hyperlink{attribute.simp}{\mbox{\isa{simp}}}, while non-trivial rules like
   \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}} are better avoided.
 
-  The \isa{kind} determines the theorem kind tag of the resulting
-  fact.  Typical examples are \verb|Thm.definitionK| or \verb|Thm.theoremK|.
-
   \item \verb|Local_Theory.note|~\isa{{\isacharparenleft}a{\isacharcomma}\ ths{\isacharparenright}\ lthy} is
   analogous to \verb|Local_Theory.define|, but defines facts instead of
   terms.  There is also a slightly more general variant \verb|Local_Theory.notes| that defines several facts (with attribute