src/Pure/tactic.ML
changeset 26626 c6231d64d264
parent 26424 a6cad32a27b0
child 27158 113a32dd0b14
     1.1 --- a/src/Pure/tactic.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -263,15 +263,19 @@
     1.4      i.e. Tinsts is not applied to insts.
     1.5  *)
     1.6  fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
     1.7 -let val {maxidx,thy,...} = rep_thm st
     1.8 +let
     1.9 +    val thy = Thm.theory_of_thm st
    1.10 +    val cert = Thm.cterm_of thy
    1.11 +    val certT = Thm.ctyp_of thy
    1.12 +    val maxidx = Thm.maxidx_of st
    1.13      val paramTs = map #2 (params_of_state i st)
    1.14 -    and inc = maxidx+1
    1.15 +    val inc = maxidx+1
    1.16      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    1.17      (*lift only Var, not term, which must be lifted already*)
    1.18 -    fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
    1.19 +    fun liftpair (v,t) = (cert (liftvar v), cert t)
    1.20      fun liftTpair (((a, i), S), T) =
    1.21 -      (ctyp_of thy (TVar ((a, i + inc), S)),
    1.22 -       ctyp_of thy (Logic.incr_tvar inc T))
    1.23 +      (certT (TVar ((a, i + inc), S)),
    1.24 +       certT (Logic.incr_tvar inc T))
    1.25  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.26                       (Thm.lift_rule (Thm.cprem_of st i) rule)
    1.27  end;