diff -r 2f39d95ac55d -r e3f2262786ea src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jul 26 21:50:44 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jul 26 22:07:37 2015 +0200
@@ -6,7 +6,7 @@
 Alternate syntax for rule_insts.ML participates in token closures by
 examining the behaviour of Rule_Insts.where_rule and instantiating token
 values accordingly. Instantiations in re-interpretation are done with
-Drule.cterm_instantiate.
+infer_instantiate.
 *)
 
 structure Eisbach_Rule_Insts: sig end =
@@ -57,13 +57,13 @@
         SOME S => (((xi, S), Thm.ctyp_of ctxt (Logic.dest_type t)) :: Ts, ts)
       | NONE =>
           (case AList.lookup (op =) tvars xi of
-            SOME T => (Ts, (Thm.cterm_of ctxt (Var (xi, T)), Thm.cterm_of ctxt t) :: ts)
+            SOME _ => (Ts, (xi, Thm.cterm_of ctxt t) :: ts)
           | NONE => error "indexname not found in thm"));
 
-    val (cTinsts, cinsts) = fold add_inst insts ([], []);
+    val (instT, inst) = fold add_inst insts ([], []);
   in
-    (Thm.instantiate (cTinsts, []) thm
-    |> Drule.cterm_instantiate cinsts
+    (Thm.instantiate (instT, []) thm
+    |> infer_instantiate ctxt inst
     COMP_INCR asm_rl)
     |> Thm.adjust_maxidx_thm ~1
     |> restore_tags thm