src/Pure/term.ML
changeset 15797 a63605582573
parent 15632 bb178a7a69c1
child 15914 2a8f86685745
     1.1 --- a/src/Pure/term.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -97,7 +97,6 @@
     1.4    val subst_bounds: term list * term -> term
     1.5    val subst_bound: term * term -> term
     1.6    val subst_TVars: (indexname * typ) list -> term -> term
     1.7 -  val subst_TVars_Vartab: typ Vartab.table -> term -> term
     1.8    val betapply: term * term -> term
     1.9    val eq_ix: indexname * indexname -> bool
    1.10    val ins_ix: indexname * indexname list -> indexname list
    1.11 @@ -113,9 +112,9 @@
    1.12    val could_unify: term * term -> bool
    1.13    val subst_free: (term * term) list -> term -> term
    1.14    val subst_atomic: (term * term) list -> term -> term
    1.15 +  val typ_subst_atomic: (typ * typ) list -> typ -> typ
    1.16    val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
    1.17    val typ_subst_TVars: (indexname * typ) list -> typ -> typ
    1.18 -  val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
    1.19    val subst_Vars: (indexname * term) list -> term -> term
    1.20    val incr_tvar: int -> typ -> typ
    1.21    val xless: (string * int) * indexname -> bool
    1.22 @@ -656,6 +655,12 @@
    1.23              | subst t = getOpt (assoc(instl,t),t)
    1.24        in  subst t  end;
    1.25  
    1.26 +(*Replace the ATOMIC type Ti by Ui;    instl = [(T1,U1), ..., (Tn,Un)].*)
    1.27 +fun typ_subst_atomic [] T = T
    1.28 +  | typ_subst_atomic instl (Type (s, Ts)) =
    1.29 +      Type (s, map (typ_subst_atomic instl) Ts)
    1.30 +  | typ_subst_atomic instl T = getOpt (assoc (instl, T), T);
    1.31 +
    1.32  (*Substitute for type Vars in a type*)
    1.33  fun typ_subst_TVars iTs T = if null iTs then T else
    1.34    let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
    1.35 @@ -1034,17 +1039,6 @@
    1.36  structure Typtab = TableFun(type key = typ val ord = typ_ord);
    1.37  structure Termtab = TableFun(type key = term val ord = term_ord);
    1.38  
    1.39 -(*Substitute for type Vars in a type, version using Vartab*)
    1.40 -fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
    1.41 -  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
    1.42 -        | subst(T as TFree _) = T
    1.43 -        | subst(T as TVar(ixn, _)) =
    1.44 -            (case Vartab.lookup (iTs, ixn) of NONE => T | SOME(U) => U)
    1.45 -  in subst T end;
    1.46 -
    1.47 -(*Substitute for type Vars in a term, version using Vartab*)
    1.48 -val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
    1.49 -
    1.50  
    1.51  (*** Compression of terms and types by sharing common subtrees.
    1.52       Saves 50-75% on storage requirements.  As it is a bit slow,