# HG changeset patch
# User wenzelm
# Date 1206628332 -3600
# Node ID d004b791218ee216c406df745f98970f29e6911d
# Parent  9c2cdf28ececa54d581ebc0d0f19958f801a1576
Command 'setup': discontinued implicit version.

diff -r 9c2cdf28ecec -r d004b791218e NEWS
--- a/NEWS	Thu Mar 27 14:41:21 2008 +0100
+++ b/NEWS	Thu Mar 27 15:32:12 2008 +0100
@@ -31,6 +31,8 @@
 
 * Eliminated theory ProtoPure.  Potential INCOMPATIBILITY.
 
+* Command 'setup': discontinued implicit version.
+
 * Instantiation target allows for simultaneous specification of class
 instance operations together with an instantiation proof.
 Type-checking phase allows to refer to class operations uniformly.
diff -r 9c2cdf28ecec -r d004b791218e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Mar 27 14:41:21 2008 +0100
+++ b/doc-src/IsarRef/pure.tex	Thu Mar 27 15:32:12 2008 +0100
@@ -483,9 +483,7 @@
 \begin{rail}
   'use' name
   ;
-  ('ML' | 'ML\_val' | 'ML\_command' | 'ML\_setup') text
-  ;
-  'setup' text?
+  ('ML' | 'ML\_val' | 'ML\_command' | 'ML\_setup' | 'setup') text
   ;
   'method\_setup' name '=' text text
   ;
@@ -509,12 +507,11 @@
   theory context is passed down to the ML session, and fetched back
   afterwards.  Thus $text$ may actually change the theory as a side effect.
   
-\item [$\isarkeyword{setup}~text$] changes the current theory context by
-  applying $text$, which refers to an ML expression of type
-  \texttt{theory~->~theory)}.  The $\isarkeyword{setup}$ command is the
-  canonical way to initialize any object-logic specific tools and packages
-  written in ML.  If the $text$ is omitted, the setup value is taken from the
-  implicit context maintained via \verb,Context.add_setup,.
+\item [$\isarkeyword{setup}~text$] changes the current theory context
+  by applying $text$, which refers to an ML expression of type
+  \texttt{theory~->~theory)}.  The $\isarkeyword{setup}$ command is
+  the canonical way to initialize any object-logic specific tools and
+  packages written in ML.
   
 \item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
   method in the current theory.  The given $text$ has to be an ML expression