src/Pure/codegen.ML

 (**** add new code generators to theory ****)
 
 fun add_codegen name f thy =
   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
     CodegenData.get thy
-  in (case assoc (codegens, name) of
+  in (case AList.lookup (op =) codegens name of
       NONE => CodegenData.put {codegens = (name, f) :: codegens,
         tycodegens = tycodegens, consts = consts, types = types,
         attrs = attrs, preprocs = preprocs, modules = modules,
         test_params = test_params} thy
     | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   end;
 
 fun add_tycodegen name f thy =
   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
     CodegenData.get thy
-  in (case assoc (tycodegens, name) of
+  in (case AList.lookup (op =) tycodegens name of
       NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
         codegens = codegens, consts = consts, types = types,
         attrs = attrs, preprocs = preprocs, modules = modules,
         test_params = test_params} thy
     | SOME _ => error ("Code generator " ^ name ^ " already declared"))

 (**** code attribute ****)
 
 fun add_attribute name att thy =
   let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
     CodegenData.get thy
-  in (case assoc (attrs, name) of
+  in (case AList.lookup (op =) attrs name of
       NONE => CodegenData.put {tycodegens = tycodegens,
         codegens = codegens, consts = consts, types = types,
         attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
         preprocs = preprocs, modules = modules,
         test_params = test_params} thy

               | SOME ty =>
                   let val U = prep_type thy ty
                   in if Sign.typ_instance thy (U, T) then U
                     else error ("Illegal type constraint for constant " ^ cname)
                   end)
-         in (case assoc (consts, (cname, T')) of
+         in (case AList.lookup (op =) consts (cname, T') of
              NONE => CodegenData.put {codegens = codegens,
                tycodegens = tycodegens,
                consts = ((cname, T'), syn) :: consts,
                types = types, attrs = attrs, preprocs = preprocs,
                modules = modules, test_params = test_params} thy

   let
     val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
       CodegenData.get thy;
     val tc = Sign.intern_type thy s
   in
-    (case assoc (types, tc) of
+    (case AList.lookup (op =) types tc of
        NONE => CodegenData.put {codegens = codegens,
          tycodegens = tycodegens, consts = consts,
          types = (tc, syn) :: types, attrs = attrs,
          preprocs = preprocs, modules = modules, test_params = test_params} thy
      | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   end) (thy, xs);
 
-fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s);
+fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
 
 
 (**** make valid ML identifiers ****)
 
 fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse

     val (illegal, alt_names) = split_list (List.mapPartial (fn s =>
       let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
     val ps = (reserved @ illegal) ~~
       variantlist (map (suffix "'") reserved @ alt_names, names);
 
-    fun rename_id s = getOpt (assoc (ps, s), s);
+    fun rename_id s = AList.lookup (op =) ps s |> the_default s;
 
     fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
       | rename (Free (a, T)) = Free (rename_id a, T)
       | rename (Abs (s, T, t)) = Abs (s, T, rename t)
       | rename (t $ u) = rename t $ rename u

 fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
       SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i)))
   | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
       SOME (gr, Pretty.str s)
   | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
-      (case assoc (#types (CodegenData.get thy), s) of
+      (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
          NONE => NONE
        | SOME (ms, aux) =>
            let
              val (gr', ps) = foldl_map
                (invoke_tycodegen thy defs dep module false)

   add_tycodegen "default" default_tycodegen];
 
 
 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
 
-fun add_to_module name s ms =
-  overwrite (ms, (name, the (assoc (ms, name)) ^ s));
+fun add_to_module name s = AList.map_entry (op =) name (suffix s);
 
 fun output_code gr module xs =
   let
     val code = List.mapPartial (fn s =>
       let val c as (_, module', _) = Graph.get_node gr s

     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
       | strip t = t;
     val (gi, frees) = Logic.goal_params
       (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
     val gi' = ObjectLogic.atomize_term thy (map_term_types
-      (map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
-        getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
+      (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
+        getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
   in case test_term (Toplevel.theory_of st) size iterations gi' of
       NONE => writeln "No counterexamples found."
     | SOME cex => writeln ("Counterexample found:\n" ^
         Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,

   [("size", P.nat >> (K o set_size)),
    ("iterations", P.nat >> (K o set_iterations)),
    ("default_type", P.typ >> set_default_type)];
 
 val parse_test_params = P.short_ident :-- (fn s =>
-  P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
+  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
 
 fun parse_tyinst xs =
   (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
     fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs;