src/Pure/proofterm.ML
changeset 15797 a63605582573
parent 15632 bb178a7a69c1
child 16458 4c6fd0c01d28
     1.1 --- a/src/Pure/proofterm.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -69,11 +69,11 @@
     1.4    (** proof terms for specific inference rules **)
     1.5    val implies_intr_proof : term -> proof -> proof
     1.6    val forall_intr_proof : term -> string -> proof -> proof
     1.7 -  val varify_proof : term -> string list -> proof -> proof
     1.8 +  val varify_proof : term -> (string * sort) list -> proof -> proof
     1.9    val freezeT : term -> proof -> proof
    1.10    val rotate_proof : term list -> term -> int -> proof -> proof
    1.11    val permute_prems_prf : term list -> int -> int -> proof -> proof
    1.12 -  val instantiate : (indexname * typ) list -> (term * term) list -> proof -> proof
    1.13 +  val instantiate : (typ * typ) list -> (term * term) list -> proof -> proof
    1.14    val lift_proof : term -> int -> term -> proof -> proof
    1.15    val assumption_proof : term list -> term -> int -> proof -> proof
    1.16    val bicompose_proof : term list -> term list -> term list -> term option ->
    1.17 @@ -401,7 +401,8 @@
    1.18    | remove_types t = t;
    1.19  
    1.20  fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
    1.21 -  Envir.Envir {iTs = iTs, asol = Vartab.map remove_types asol, maxidx = maxidx};
    1.22 +  Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
    1.23 +    maxidx = maxidx};
    1.24  
    1.25  fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
    1.26  
    1.27 @@ -530,11 +531,11 @@
    1.28  
    1.29  fun varify_proof t fixed prf =
    1.30    let
    1.31 -    val fs = add_term_tfree_names (t, []) \\ fixed;
    1.32 +    val fs = add_term_tfrees (t, []) \\ fixed;
    1.33      val ixns = add_term_tvar_ixns (t, []);
    1.34 -    val fmap = fs ~~ variantlist (fs, map #1 ixns)
    1.35 +    val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
    1.36      fun thaw (f as (a, S)) =
    1.37 -      (case assoc (fmap, a) of
    1.38 +      (case assoc (fmap, f) of
    1.39          NONE => TFree f
    1.40        | SOME b => TVar ((b, 0), S));
    1.41    in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
    1.42 @@ -598,7 +599,7 @@
    1.43  
    1.44  fun instantiate vTs tpairs prf =
    1.45    map_proof_terms (subst_atomic (map (apsnd remove_types) tpairs) o
    1.46 -    subst_TVars vTs) (typ_subst_TVars vTs) prf;
    1.47 +    map_term_types (typ_subst_atomic vTs)) (typ_subst_atomic vTs) prf;
    1.48  
    1.49  
    1.50  (***** lifting *****)
    1.51 @@ -955,7 +956,7 @@
    1.52  
    1.53  fun prf_subst (pinst, (tyinsts, insts)) =
    1.54    let
    1.55 -    val substT = typ_subst_TVars_Vartab tyinsts;
    1.56 +    val substT = Envir.typ_subst_TVars tyinsts;
    1.57  
    1.58      fun subst' lev (t as Var (ixn, _)) = (case assoc (insts, ixn) of
    1.59            NONE => t