diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Mon Jun 16 22:13:39 2008 +0200
@@ -24,10 +24,10 @@
   (* ------------------------------------------------------------------------- *)
   (* Useful Theorems                                                           *)
   (* ------------------------------------------------------------------------- *)
-  val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE);
+  val EXCLUDED_MIDDLE = rotate_prems 1 (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 = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
+  val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
 
   (* ------------------------------------------------------------------------- *)
   (* Useful Functions                                                          *)