src/Pure/type.ML
changeset 17184 3d80209e9a53
parent 16946 7f9a7fe413f3
child 17221 6cd180204582
     1.1 --- a/src/Pure/type.ML	Mon Aug 29 16:18:03 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Mon Aug 29 16:18:04 2005 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4  local
     1.5  
     1.6  fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
     1.7 -  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
     1.8 +  | inst_typ env (T as TFree (x, _)) = if_none (AList.lookup (op =) env x) T
     1.9    | inst_typ _ T = T;
    1.10  
    1.11  fun certify_typ normalize syntax tsig ty =
    1.12 @@ -223,7 +223,7 @@
    1.13      val ixns = add_term_tvar_ixns (t, []);
    1.14      val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
    1.15      fun thaw (f as (a, S)) =
    1.16 -      (case gen_assoc (op =) (fmap, f) of
    1.17 +      (case AList.lookup (op =) fmap f of
    1.18          NONE => TFree f
    1.19        | SOME xi => TVar (xi, S));
    1.20    in (map_term_types (map_type_tfree thaw) t, fmap) end;
    1.21 @@ -238,11 +238,11 @@
    1.22    in ((ix, v) :: pairs, v :: used) end;
    1.23  
    1.24  fun freeze_one alist (ix, sort) =
    1.25 -  TFree (the (assoc_string_int (alist, ix)), sort)
    1.26 +  TFree (the (AList.lookup (op =) alist ix), sort)
    1.27      handle Option =>
    1.28        raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
    1.29  
    1.30 -fun thaw_one alist (a, sort) = TVar (the (assoc_string (alist, a)), sort)
    1.31 +fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
    1.32    handle Option => TFree (a, sort);
    1.33  
    1.34  in
    1.35 @@ -464,7 +464,7 @@
    1.36    end;
    1.37  
    1.38  fun insert pp C t (c, Ss) ars =
    1.39 -  (case assoc_string (ars, c) of
    1.40 +  (case AList.lookup (op =) ars c of
    1.41      NONE => coregular pp C t (c, Ss) ars
    1.42    | SOME Ss' =>
    1.43        if Sorts.sorts_le C (Ss, Ss') then ars