src/Pure/type.ML

 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
 local
 
 fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
-  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
+  | inst_typ env (T as TFree (x, _)) = if_none (AList.lookup (op =) env x) T
   | inst_typ _ T = T;
 
 fun certify_typ normalize syntax tsig ty =
   let
     val TSig {classes = (_, classes), types = (_, types), ...} = tsig;

   let
     val fs = add_term_tfrees (t, []) \\ fixed;
     val ixns = add_term_tvar_ixns (t, []);
     val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
     fun thaw (f as (a, S)) =
-      (case gen_assoc (op =) (fmap, f) of
+      (case AList.lookup (op =) fmap f of
         NONE => TFree f
       | SOME xi => TVar (xi, S));
   in (map_term_types (map_type_tfree thaw) t, fmap) end;
 
 

 fun new_name (ix, (pairs, used)) =
   let val v = variant used (string_of_indexname ix)
   in ((ix, v) :: pairs, v :: used) end;
 
 fun freeze_one alist (ix, sort) =
-  TFree (the (assoc_string_int (alist, ix)), sort)
+  TFree (the (AList.lookup (op =) alist ix), sort)
     handle Option =>
       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
 
-fun thaw_one alist (a, sort) = TVar (the (assoc_string (alist, a)), sort)
+fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
   handle Option => TFree (a, sort);
 
 in
 
 (*this sort of code could replace unvarifyT*)

       SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
     | NONE => (c, Ss) :: ars)
   end;
 
 fun insert pp C t (c, Ss) ars =
-  (case assoc_string (ars, c) of
+  (case AList.lookup (op =) ars c of
     NONE => coregular pp C t (c, Ss) ars
   | SOME Ss' =>
       if Sorts.sorts_le C (Ss, Ss') then ars
       else if Sorts.sorts_le C (Ss', Ss)
       then coregular pp C t (c, Ss) (ars \ (c, Ss'))