src/HOL/Tools/record_package.ML

         fun bad_inst ((x, S), T) =
           if Sign.of_sort sign (T, S) then NONE else SOME x
         val bads = List.mapPartial bad_inst (args ~~ types);
 
         val inst = map fst args ~~ types;
-        val subst = Term.map_type_tfree (fn (x, _) => valOf (assoc (inst, x)));
+        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
         val parent' = Option.map (apfst (map subst)) parent;
         val fields' = map (apsnd subst) fields;
         val extension' = apsnd (map subst) extension;
       in
         conditional (not (null bads)) (fn () =>

           else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
       | splitargs [] (fargs as (_::_)) = ([],fargs)
       | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
       | splitargs _ _ = ([],[]);
 
-    fun get_sort xs n = (case assoc (xs,n) of
-                                SOME s => s
-                              | NONE => Sign.defaultS sg);
-
+    fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS sg);
 
     fun to_type t = Sign.certify_typ sg
                        (Sign.intern_typ sg
                          (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t));
 

 fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg tm =
   let
       (* tm is term representation of a (nested) field type. We first reconstruct the      *)
       (* type from tm so that we can continue on the type level rather then the term level.*)
 
-      fun get_sort xs n = (case assoc (xs,n) of
-                             SOME s => s
-                           | NONE => Sign.defaultS sg);
+      fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS sg);
 
       (* WORKAROUND:
        * If a record type occurs in an error message of type inference there
        * may be some internal frees donoted by ??:
        * (Const "_tfree",_)$Free ("??'a",_).

        else default_tr' sg tm
   end
 
 fun record_type_tr' sep mark record record_scheme sg t =
   let
-    fun get_sort xs n = (case assoc (xs,n) of
-                             SOME s => s
-                           | NONE => Sign.defaultS sg);
+    fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS sg);
 
     val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
 
     fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
 

     Type (name, Ts) => (Ts, name)
   | _ => error ("Bad parent record specification: " ^ quote s));
 
 fun read_typ sign (env, s) =
   let
-    fun def_sort (x, ~1) = assoc (env, x)
+    fun def_sort (x, ~1) = AList.lookup (op =) env x
       | def_sort _ = NONE;
     val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
   in (Term.add_typ_tfrees (T, env), T) end;
 
 fun cert_typ sign (env, raw_T) =

     val (x, ca) = (case rev (Library.drop (length params, ys)) of
         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
       | [x] => (head_of x, false));
     val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
-        [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
+        [] => (case AList.lookup (op =) (map dest_Free (term_frees (prop_of st))) s of
           NONE => sys_error "try_param_tac: no such variable"
         | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl),
             (x, Free (s, T))])
       | (_, T) :: _ => [(P, list_abs (params, if ca then concl
           else incr_boundvars 1 (Abs (s, T, concl)))),