src/Pure/tactic.ML

     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
       | types'(ixn) = types ixn;
     val used = add_term_tvarnames
                   (#prop(rep_thm st) $ #prop(rep_thm rule),[])
     val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
-in instantiate (map lifttvar Tinsts, map liftpair insts)
-               (lift_rule (st,i) rule)
+in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
+                     (lift_rule (st,i) rule)
 end;
 
 (*
 Like lift_inst_rule but takes terms, not strings, where the terms may contain
 Bounds referring to parameters of the subgoal.

     and inc = maxidx+1
     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
     (*lift only Var, not term, which must be lifted already*)
     fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
     fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
-in instantiate (map liftTpair Tinsts, map liftpair insts)
-               (lift_rule (st,i) rule)
+in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
+                     (lift_rule (st,i) rule)
 end;
 
 (*** Resolve after lifting and instantation; may refer to parameters of the
      subgoal.  Fails if "i" is out of range.  ***)