1.1 --- a/src/Provers/hypsubst.ML	Sat May 24 22:19:35 2008 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Sat May 24 23:52:35 2008 +0200
     1.3 @@ -143,33 +143,35 @@
     1.4  
     1.5  val ssubst = standard (Data.sym RS Data.subst);
     1.6  
     1.7 -fun inst_subst_tac b rl = SUBGOAL (fn (Bi, i) => fn st =>
     1.8 +fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
     1.9    case try (Logic.strip_assums_hyp #> hd #>
    1.10 -      Data.dest_Trueprop #> Data.dest_eq #> pairself contract) Bi of
    1.11 +      Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
    1.12      SOME (t, t') =>
    1.13        let
    1.14 +        val Bi = Thm.term_of cBi;
    1.15          val ps = Logic.strip_params Bi;
    1.16 -        val U = fastype_of1 (rev (map snd ps), t);
    1.17 +        val U = Term.fastype_of1 (rev (map snd ps), t);
    1.18          val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
    1.19 -        val rl' = Thm.lift_rule (nth (cprems_of st) (i - 1)) rl;
    1.20 -        val Var (ixn, T) = head_of (Data.dest_Trueprop
    1.21 -          (Logic.strip_assums_concl (prop_of rl')));
    1.22 +        val rl' = Thm.lift_rule cBi rl;
    1.23 +        val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
    1.24 +          (Logic.strip_assums_concl (Thm.prop_of rl')));
    1.25          val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
    1.26 -          (Logic.strip_assums_concl (hd (prems_of rl'))));
    1.27 -        val (Ts, V) = split_last (binder_types T);
    1.28 +          (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
    1.29 +        val (Ts, V) = split_last (Term.binder_types T);
    1.30          val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
    1.31              Bound j => subst_bounds (map Bound
    1.32                ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
    1.33 -          | t => abstract_over (t, incr_boundvars 1 Q));
    1.34 -        val thy = theory_of_thm rl'
    1.35 -      in compose_tac (true, instantiate ([(ctyp_of thy V, ctyp_of thy U)],
    1.36 +          | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
    1.37 +        val thy = Thm.theory_of_thm rl';
    1.38 +        val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
    1.39 +      in compose_tac (true, Drule.instantiate (instT,
    1.40          map (pairself (cterm_of thy))
    1.41            [(Var (ixn, Ts ---> U --> body_type T), u),
    1.42             (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
    1.43             (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
    1.44 -        nprems_of rl) i st
    1.45 +        nprems_of rl) i
    1.46        end
    1.47 -  | NONE => Seq.empty);
    1.48 +  | NONE => no_tac);
    1.49  
    1.50  val imp_intr_tac = rtac Data.imp_intr;
    1.51