diff -r 4dce06387aea -r c0cfc4ac12e2 src/Pure/tactic.ML
--- 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;