RuleInsts.read_instantiate;

--- a/src/HOL/Tools/TFL/post.ML	Mon Jun 16 17:54:42 2008 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Mon Jun 16 17:54:43 2008 +0200
@@ -152,7 +152,7 @@
   rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
 
 (*Strip off the outer !P*)
-val spec'= Drule.read_instantiate [("x","P::?'b=>bool")] spec;
+val spec'= RuleInsts.read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
 
 fun tracing true _ = ()
   | tracing false msg = writeln msg;

--- a/src/HOL/Tools/meson.ML	Mon Jun 16 17:54:42 2008 +0200
+++ b/src/HOL/Tools/meson.ML	Mon Jun 16 17:54:43 2008 +0200
@@ -646,7 +646,7 @@
 (*Rules to convert the head literal into a negated assumption. If the head
   literal is already negated, then using notEfalse instead of notEfalse'
   prevents a double negation.*)
-val notEfalse = Drule.read_instantiate [("R","False")] notE;
+val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
 val notEfalse' = rotate_prems 1 notEfalse;
 
 fun negated_asm_of_head th =

--- a/src/HOL/Tools/metis_tools.ML	Mon Jun 16 17:54:42 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Mon Jun 16 17:54:43 2008 +0200
@@ -24,10 +24,10 @@
   (* ------------------------------------------------------------------------- *)
   (* Useful Theorems                                                           *)
   (* ------------------------------------------------------------------------- *)
-  val EXCLUDED_MIDDLE  = rotate_prems 1 (Drule.read_instantiate [("R","False")] notE);
-  val REFL_THM         = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
+  val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE);
+  val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
   val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
-  val ssubst_em  = Drule.read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
+  val ssubst_em = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
 
   (* ------------------------------------------------------------------------- *)
   (* Useful Functions                                                          *)

--- a/src/ZF/ind_syntax.ML	Mon Jun 16 17:54:42 2008 +0200
+++ b/src/ZF/ind_syntax.ML	Mon Jun 16 17:54:43 2008 +0200
@@ -51,7 +51,7 @@
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)
 val equals_CollectD =
-    Drule.read_instantiate [("W","?Q")]
+    RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));