# HG changeset patch
# User paulson
# Date 869651339 -7200
# Node ID 329441e7eeee208b913b1e4174fee35498567932
# Parent  7db9a44dfa0629645328ff7cbe9688e512ad01b0
Removal of tactical STATE

diff -r 7db9a44dfa06 -r 329441e7eeee NEWS
--- a/NEWS	Wed Jul 23 11:11:14 1997 +0200
+++ b/NEWS	Wed Jul 23 11:48:59 1997 +0200
@@ -13,6 +13,9 @@
 
 * improved output of warnings / errors;
 
+* deleted the obsolete tactical STATE, which was declared by
+	fun STATE tacfun st = tacfun st st;
+
 
 New in Isabelle94-8 (May 1997)
 ------------------------------
diff -r 7db9a44dfa06 -r 329441e7eeee doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Wed Jul 23 11:11:14 1997 +0200
+++ b/doc-src/Ref/tactic.tex	Wed Jul 23 11:48:59 1997 +0200
@@ -564,31 +564,23 @@
 really need to code tactics from scratch.
 
 \subsection{Operations on type {\tt tactic}}
-\index{tactics!primitives for coding}
-A tactic maps theorems to theorem sequences (lazy lists).  The type
-constructor for sequences is called \mltydx{Sequence.seq}.  To simplify the
-types of tactics and tacticals, Isabelle defines a type abbreviations:
+\index{tactics!primitives for coding} A tactic maps theorems to sequences of
+theorems.  The type constructor for sequences (lazy lists) is called
+\mltydx{Sequence.seq}.  To simplify the types of tactics and tacticals,
+Isabelle defines a type abbreviation:
 \begin{ttbox} 
 type tactic = thm -> thm Sequence.seq
 \end{ttbox} 
 The following operations provide means for coding tactics in a clean style.
 \begin{ttbox} 
 PRIMITIVE :                  (thm -> thm) -> tactic  
-STATE     :               (thm -> tactic) -> tactic
 SUBGOAL   : ((term*int) -> tactic) -> int -> tactic
 \end{ttbox} 
 \begin{ttdescription}
-\item[\ttindexbold{PRIMITIVE} $f$] 
-applies $f$ to the proof state and returns the result as a
-one-element sequence.  This packages the meta-rule~$f$ as a tactic.
-
-\item[\ttindexbold{STATE} $f$] 
-applies $f$ to the proof state and then applies the resulting tactic to the
-same state.  It supports the following style, where the tactic body is
-expressed using tactics and tacticals, but may peek at the proof state:
-\begin{ttbox} 
-STATE (fn state => {\it tactic-valued expression})
-\end{ttbox} 
+\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
+  applies $f$ to the proof state and returns the result as a one-element
+  sequence.  If $f$ raises an exception, then the tactic's result is the empty
+  sequence.
 
 \item[\ttindexbold{SUBGOAL} $f$ $i$] 
 extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
diff -r 7db9a44dfa06 -r 329441e7eeee src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Jul 23 11:11:14 1997 +0200
+++ b/src/Pure/tctical.ML	Wed Jul 23 11:48:59 1997 +0200
@@ -49,7 +49,6 @@
   val REPEAT_SOME       : (int -> tactic) -> tactic
   val SELECT_GOAL       : tactic -> int -> tactic
   val SOMEGOAL          : (int -> tactic) -> tactic   
-  val STATE             : (thm -> tactic) -> tactic
   val strip_context     : term -> (string * typ) list * term list * term
   val SUBGOAL           : ((term*int) -> tactic) -> int -> tactic
   val suppress_tracing  : bool ref
@@ -75,9 +74,6 @@
 
 type tactic = thm -> thm Sequence.seq;
 
-(*Makes a tactic from one that uses the components of the state.*)
-fun STATE tacfun st = tacfun st st;
-
 
 (*** LCF-style tacticals ***)