src/Pure/term.ML
changeset 17314 04e21a27c0ad
parent 17271 2756a73f63a5
child 17642 e063c0403650
     1.1 --- a/src/Pure/term.ML	Thu Sep 08 16:08:50 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Sep 08 16:09:23 2005 +0200
     1.3 @@ -861,7 +861,7 @@
     1.4  fun subst_free [] = (fn t=>t)
     1.5    | subst_free pairs =
     1.6        let fun substf u =
     1.7 -            case gen_assoc (op aconv) (pairs, u) of
     1.8 +            case AList.lookup (op aconv) pairs u of
     1.9                  SOME u' => u'
    1.10                | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
    1.11                                   | t$u' => substf t $ substf u'
    1.12 @@ -916,7 +916,7 @@
    1.13        let
    1.14          fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
    1.15            | subst (t $ u) = subst t $ subst u
    1.16 -          | subst t = if_none (gen_assoc (op aconv) (inst, t)) t;
    1.17 +          | subst t = if_none (AList.lookup (op aconv) inst t) t;
    1.18        in subst tm end;
    1.19  
    1.20  (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
    1.21 @@ -924,7 +924,7 @@
    1.22    | typ_subst_atomic inst ty =
    1.23        let
    1.24          fun subst (Type (a, Ts)) = Type (a, map subst Ts)
    1.25 -          | subst T = if_none (gen_assoc (op = : typ * typ -> bool) (inst, T)) T;
    1.26 +          | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
    1.27        in subst ty end;
    1.28  
    1.29  fun subst_atomic_types [] tm = tm
    1.30 @@ -977,7 +977,7 @@
    1.31        let
    1.32          fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
    1.33            | subst_typ (TVar v) =
    1.34 -              (case gen_assoc eq_tvar (instT, v) of
    1.35 +              (case AList.lookup eq_tvar instT v of
    1.36                  SOME T => T
    1.37                | NONE => raise SAME)
    1.38            | subst_typ _ = raise SAME
    1.39 @@ -995,7 +995,7 @@
    1.40            | subst (Free (x, T)) = Free (x, substT T)
    1.41            | subst (Var (xi, T)) =
    1.42                let val (T', same) = (substT T, false) handle SAME => (T, true) in
    1.43 -                (case gen_assoc eq_var (inst, (xi, T')) of
    1.44 +                (case AList.lookup eq_var inst (xi, T') of
    1.45                     SOME t => t
    1.46                   | NONE => if same then raise SAME else Var (xi, T'))
    1.47                end