--- a/src/Pure/tactic.ML Thu Apr 10 20:54:18 2008 +0200
+++ b/src/Pure/tactic.ML Sat Apr 12 17:00:35 2008 +0200
@@ -263,15 +263,19 @@
i.e. Tinsts is not applied to insts.
*)
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
-let val {maxidx,thy,...} = rep_thm st
+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)
- and inc = maxidx+1
+ 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) = (cterm_of thy (liftvar v), cterm_of thy t)
+ fun liftpair (v,t) = (cert (liftvar v), cert t)
fun liftTpair (((a, i), S), T) =
- (ctyp_of thy (TVar ((a, i + inc), S)),
- ctyp_of thy (Logic.incr_tvar inc 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;