--- 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