src/Pure/tactic.ML

                                     Logic.incr_indexes(paramTs,inc) t)
     (*Lifts instantiation pair over params*)
     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
     val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
-                     (lift_rule (st,i) rule)
+                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
 end;
 
 fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
   (st, i, map (apfst Syntax.indexname) sinsts, rule);
 

     fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
     fun liftTpair (((a, i), S), T) =
       (ctyp_of thy (TVar ((a, i + inc), S)),
        ctyp_of thy (Logic.incr_tvar inc T))
 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
-                     (lift_rule (st,i) rule)
+                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
 end;
 
 (*** Resolve after lifting and instantation; may refer to parameters of the
      subgoal.  Fails if "i" is out of range.  ***)
 

 
 (*meta-level conjunction*)
 val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $
       (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) =>
     (fn st =>
-      compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st)
+      compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
   | _ => no_tac);
 
 val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
 
 fun smart_conjunction_tac 0 = assume_tac 1