added instantiate_tac

--- a/doc-src/Ref/tactic.tex	Fri Oct 27 15:23:39 2000 +0200
+++ b/doc-src/Ref/tactic.tex	Fri Oct 27 15:53:47 2000 +0200
@@ -105,20 +105,24 @@
 \end{ttdescription}
 
 
-\subsection{Resolution with instantiation} \label{res_inst_tac}
+\subsection{Explicit instantiation} \label{res_inst_tac}
 \index{tactics!instantiation}\index{instantiation}
 \begin{ttbox} 
-res_inst_tac  : (string*string)list -> thm -> int -> tactic
-eres_inst_tac : (string*string)list -> thm -> int -> tactic
-dres_inst_tac : (string*string)list -> thm -> int -> tactic
-forw_inst_tac : (string*string)list -> thm -> int -> tactic
+res_inst_tac    : (string*string)list -> thm -> int -> tactic
+eres_inst_tac   : (string*string)list -> thm -> int -> tactic
+dres_inst_tac   : (string*string)list -> thm -> int -> tactic
+forw_inst_tac   : (string*string)list -> thm -> int -> tactic
+instantiate_tac : (string*string)list -> tactic
 \end{ttbox}
-These tactics are designed for applying rules such as substitution and
-induction, which cause difficulties for higher-order unification.  The
-tactics accept explicit instantiations for unknowns in the rule ---
-typically, in the rule's conclusion.  Each instantiation is a pair
-{\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading
-question mark!
+The first four of these tactics are designed for applying rules by resolution
+such as substitution and induction, which cause difficulties for higher-order 
+unification.  The tactics accept explicit instantiations for unknowns 
+in the rule ---typically, in the rule's conclusion. The last one, 
+{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state,
+independently of rule application. 
+
+Each instantiation is a pair {\tt($v$,$e$)}, 
+where $v$ is an unknown \emph{without} its leading question mark!
 \begin{itemize}
 \item If $v$ is the type unknown {\tt'a}, then
 the rule must contain a type unknown \verb$?'a$ of some
@@ -138,7 +142,7 @@
 \texttt{[("t","True")]}.  Type unknowns in the proof state may cause
 failure because the tactics cannot instantiate them.
 
-The instantiation tactics act on a given subgoal.  Terms in the
+The first four instantiation tactics act on a given subgoal.  Terms in the
 instantiations are type-checked in the context of that subgoal --- in
 particular, they may refer to that subgoal's parameters.  Any unknowns in
 the terms receive subscripts and are lifted over the parameters; thus, you
@@ -161,6 +165,10 @@
 is like {\tt dres_inst_tac} except that the selected assumption is not
 deleted.  It applies the instantiated rule to an assumption, adding the
 result as a new assumption.
+
+\item[\ttindexbold{instantiate_tac} {\it insts}] 
+instantiates unknowns in the proof state. This affects the main goal as 
+well as all subgoals.
 \end{ttdescription}
 
 

--- a/src/Pure/tactic.ML	Fri Oct 27 15:23:39 2000 +0200
+++ b/src/Pure/tactic.ML	Fri Oct 27 15:53:47 2000 +0200
@@ -96,6 +96,7 @@
   val term_lift_inst_rule	:
       thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
       -> thm
+  val instantiate_tac   : (string * string) list -> tactic
   val thin_tac		: string -> int -> tactic
   val trace_goalno_tac	: (int -> tactic) -> int -> tactic
   end;
@@ -305,6 +306,9 @@
 (*dresolve tactic applies a RULE to replace an assumption*)
 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
 
+(*instantiate variables in the whole state*)
+val instantiate_tac = PRIMITIVE o read_instantiate;
+
 (*Deletion of an assumption*)
 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;