accomodate simplified Thm.lift_rule;
authorwenzelm
Fri Oct 28 22:28:03 2005 +0200 (2005-10-28)
changeset 180345351a1538ea5
parent 18033 ab8803126f84
child 18035 eaae44affc9e
accomodate simplified Thm.lift_rule;
tuned;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Oct 28 22:28:02 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Oct 28 22:28:03 2005 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
     1.5      val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
     1.6  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
     1.7 -                     (lift_rule (st,i) rule)
     1.8 +                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
     1.9  end;
    1.10  
    1.11  fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
    1.12 @@ -285,7 +285,7 @@
    1.13        (ctyp_of thy (TVar ((a, i + inc), S)),
    1.14         ctyp_of thy (Logic.incr_tvar inc T))
    1.15  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.16 -                     (lift_rule (st,i) rule)
    1.17 +                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
    1.18  end;
    1.19  
    1.20  (*** Resolve after lifting and instantation; may refer to parameters of the
    1.21 @@ -636,7 +636,7 @@
    1.22  val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $
    1.23        (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) =>
    1.24      (fn st =>
    1.25 -      compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st)
    1.26 +      compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
    1.27    | _ => no_tac);
    1.28  
    1.29  val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);