diff -r 3a5864b465e2 -r 29e239c7b8c2 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jan 14 12:17:53 2000 +0100
+++ b/src/Pure/tactic.ML	Mon Jan 17 14:10:32 2000 +0100
@@ -222,8 +222,8 @@
     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;
 
 (*
@@ -251,8 +251,8 @@
     (*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