# HG changeset patch
# User wenzelm
# Date 1267882506 -3600
# Node ID 07a8904f8fcd67ae0849df6e632944189007b18d
# Parent  a5b7a09034411aa768bb11d015d8312cf565ad24
removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);

diff -r a5b7a0903441 -r 07a8904f8fcd src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Mar 06 14:28:31 2010 +0100
+++ b/src/Pure/tactic.ML	Sat Mar 06 14:35:06 2010 +0100
@@ -63,8 +63,6 @@
 sig
   include BASIC_TACTIC
   val innermost_params: int -> thm -> (string * typ) list
-  val term_lift_inst_rule:
-    thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
   val insert_tagged_brl: 'a * (bool * thm) ->
     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
@@ -193,40 +191,6 @@
 (*params of subgoal i as they are printed*)
 fun params_of_state i st = rev (innermost_params i st);
 
-(*
-Like lift_inst_rule but takes terms, not strings, where the terms may contain
-Bounds referring to parameters of the subgoal.
-
-insts: [...,(vj,tj),...]
-
-The tj may contain references to parameters of subgoal i of the state st
-in the form of Bound k, i.e. the tj may be subterms of the subgoal.
-To saturate the lose bound vars, the tj are enclosed in abstractions
-corresponding to the parameters of subgoal i, thus turning them into
-functions. At the same time, the types of the vj are lifted.
-
-NB: the types in insts must be correctly instantiated already,
-    i.e. Tinsts is not applied to insts.
-*)
-fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
-let
-    val thy = Thm.theory_of_thm st
-    val cert = Thm.cterm_of thy
-    val certT = Thm.ctyp_of thy
-    val maxidx = Thm.maxidx_of st
-    val paramTs = map #2 (params_of_state i st)
-    val inc = maxidx+1
-    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
-    (*lift only Var, not term, which must be lifted already*)
-    fun liftpair (v,t) = (cert (liftvar v), cert t)
-    fun liftTpair (((a, i), S), T) =
-      (certT (TVar ((a, i + inc), S)),
-       certT (Logic.incr_tvar inc T))
-in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
-                     (Thm.lift_rule (Thm.cprem_of st i) rule)
-end;
-
-
 
 (*** Applications of cut_rl ***)