# HG changeset patch
# User wenzelm
# Date 1281545046 -7200
# Node ID fed4e71a8c0f2729b9f7481dd38ffd02ff559c9a
# Parent  d98baa2cf58929f9a94badc5277351d0b56c6559
Named_Target;

diff -r d98baa2cf589 -r fed4e71a8c0f doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Wed Aug 11 18:41:06 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Wed Aug 11 18:44:06 2010 +0200
@@ -97,7 +97,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string option -> 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 ->
@@ -114,7 +114,7 @@
   with operations on expecting a regular @{text "ctxt:"}~@{ML_type
   Proof.context}.
 
-  \item @{ML Theory_Target.init}~@{text "NONE thy"} initializes a
+  \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a
   trivial local theory from the given background theory.
   Alternatively, @{text "SOME name"} may be given to initialize a
   @{command locale} or @{command class} context (a fully-qualified
diff -r d98baa2cf589 -r fed4e71a8c0f doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Wed Aug 11 18:41:06 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Wed Aug 11 18:44:06 2010 +0200
@@ -123,7 +123,7 @@
 \begin{isamarkuptext}%
 \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}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex]
   \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%
@@ -139,7 +139,7 @@
   any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
   with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
 
-  \item \verb|Theory_Target.init|~\isa{NONE\ thy} initializes a
+  \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a
   trivial local theory from the given background theory.
   Alternatively, \isa{SOME\ name} may be given to initialize a
   \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified