src/Pure/proofterm.ML
changeset 16880 411d91d104c4
parent 16787 b6b6e2faaa41
child 16940 d14ec6f2d29b
     1.1 --- a/src/Pure/proofterm.ML	Tue Jul 19 17:21:51 2005 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Jul 19 17:21:52 2005 +0200
     1.3 @@ -73,7 +73,8 @@
     1.4    val freezeT : term -> proof -> proof
     1.5    val rotate_proof : term list -> term -> int -> proof -> proof
     1.6    val permute_prems_prf : term list -> int -> int -> proof -> proof
     1.7 -  val instantiate : (typ * typ) list -> (term * term) list -> proof -> proof
     1.8 +  val instantiate : ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     1.9 +    -> proof -> proof
    1.10    val lift_proof : term -> int -> term -> proof -> proof
    1.11    val assumption_proof : term list -> term -> int -> proof -> proof
    1.12    val bicompose_proof : term list -> term list -> term list -> term option ->
    1.13 @@ -597,9 +598,9 @@
    1.14  
    1.15  (***** instantiation *****)
    1.16  
    1.17 -fun instantiate vTs tpairs prf =
    1.18 -  map_proof_terms (subst_atomic (map (apsnd remove_types) tpairs) o
    1.19 -    map_term_types (typ_subst_atomic vTs)) (typ_subst_atomic vTs) prf;
    1.20 +fun instantiate (instT, inst) prf =
    1.21 +  map_proof_terms (Term.instantiate (instT, map (apsnd remove_types) inst))
    1.22 +    (Term.instantiateT instT) prf;
    1.23  
    1.24  
    1.25  (***** lifting *****)
    1.26 @@ -611,7 +612,7 @@
    1.27      fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
    1.28  
    1.29      fun lift' Us Ts (Abst (s, T, prf)) =
    1.30 -          (Abst (s, apsome' (same (incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
    1.31 +          (Abst (s, apsome' (same (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
    1.32             handle SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
    1.33        | lift' Us Ts (AbsP (s, t, prf)) =
    1.34            (AbsP (s, apsome' (same (lift'' Us Ts)) t, lifth' Us Ts prf)
    1.35 @@ -621,9 +622,9 @@
    1.36        | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
    1.37            handle SAME => prf1 %% lift' Us Ts prf2)
    1.38        | lift' _ _ (PThm (s, prf, prop, Ts)) =
    1.39 -          PThm (s, prf, prop, apsome' (same (map (incr_tvar inc))) Ts)
    1.40 +          PThm (s, prf, prop, apsome' (same (map (Logic.incr_tvar inc))) Ts)
    1.41        | lift' _ _ (PAxm (s, prop, Ts)) =
    1.42 -          PAxm (s, prop, apsome' (same (map (incr_tvar inc))) Ts)
    1.43 +          PAxm (s, prop, apsome' (same (map (Logic.incr_tvar inc))) Ts)
    1.44        | lift' _ _ _ = raise SAME
    1.45      and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
    1.46