# HG changeset patch
# User haftmann
# Date 1127225854 -7200
# Node ID 0f1c48de39f59975b3ea451e3d80302b30c53595
# Parent  8581c151adea11d7e2159c3cf96b2a4a92a034ef
introduced AList module in favor of assoc etc.

diff -r 8581c151adea -r 0f1c48de39f5 src/FOL/eqrule_FOL_data.ML
--- a/src/FOL/eqrule_FOL_data.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/FOL/eqrule_FOL_data.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -36,8 +36,8 @@
            Const("Trueprop",_) $ p =>
              (case Term.head_of p of
                 Const(a,_) =>
-                  (case Library.assoc(pairs,a) of
-                     SOME(rls) => List.concat (map atoms ([th] RL rls))
+                  (case AList.lookup (op =) pairs a of
+                     SOME rls => List.concat (map atoms ([th] RL rls))
                    | NONE => [th])
               | _ => [th])
          | _ => [th])
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -467,12 +467,12 @@
      else HOLogic.false_const)
       handle _ => at)
     else
-  case assoc (operations,p) of 
+  case AList.lookup (op =) operations p of 
     SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-  case assoc (operations,p) of 
+  case AList.lookup (op =) operations p of 
     SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
     HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Integ/reflected_cooper.ML
--- a/src/HOL/Integ/reflected_cooper.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -10,7 +10,7 @@
 
 fun i_of_term vs t = 
     case t of
-	Free(xn,xT) => (case assoc(vs,t) of 
+	Free(xn,xT) => (case AList.lookup (op =) vs t of 
 			   NONE   => error "Variable not found in the list!!"
 			 | SOME n => Var n)
       | Const("0",iT) => Cst 0
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Matrix/cplex/Cplex_tools.ML
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -969,10 +969,10 @@
 	val header = readHeader () 
 
 	val result = 
-	    case assoc (header, "STATUS") of
+	    case AList.lookup (op =) header "STATUS" of
 		SOME "INFEASIBLE" => Infeasible
 	      | SOME "UNBOUNDED" => Unbounded
-	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
+	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
 					   (skip_until_sep (); 
 					    skip_until_sep ();
 					    load_values ()))
@@ -1118,10 +1118,10 @@
 	val header = readHeader ()
 
 	val result = 
-	    case assoc (header, "STATUS") of
+	    case AList.lookup (op =) header "STATUS" of
 		SOME "INFEASIBLE" => Infeasible
 	      | SOME "NONOPTIMAL" => Unbounded
-	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
+	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
 					   (skip_paragraph (); 
 					    skip_paragraph (); 
 					    skip_paragraph (); 
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -467,12 +467,12 @@
      else HOLogic.false_const)
       handle _ => at)
     else
-  case assoc (operations,p) of 
+  case AList.lookup (op =) operations p of 
     SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-  case assoc (operations,p) of 
+  case AList.lookup (op =) operations p of 
     SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
     HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/Presburger/reflected_cooper.ML
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -10,7 +10,7 @@
 
 fun i_of_term vs t = 
     case t of
-	Free(xn,xT) => (case assoc(vs,t) of 
+	Free(xn,xT) => (case AList.lookup (op =) vs t of 
 			   NONE   => error "Variable not found in the list!!"
 			 | SOME n => Var n)
       | Const("0",iT) => Cst 0
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -26,7 +26,7 @@
 
 fun find_nonempty (descr: DatatypeAux.descr) is i =
   let
-    val (_, _, constrs) = valOf (assoc (descr, i));
+    val (_, _, constrs) = valOf (AList.lookup (op =) descr i);
     fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE
           else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
       | arg_nonempty _ = SOME 0;
@@ -160,7 +160,7 @@
                  [Pretty.block [Pretty.str "(case", Pretty.brk 1,
                    Pretty.str "i", Pretty.brk 1, Pretty.str "of",
                    Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
-                   mk_constr "0" true (cname, valOf (assoc (cs, cname))),
+                   mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
                    Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
                    mk_choice cs1, Pretty.str ")"]]
                else [mk_choice cs2])) ::
@@ -263,15 +263,15 @@
    (c as Const (s, T), ts) =>
        (case find_first (fn (_, {index, descr, case_name, ...}) =>
          s = case_name orelse
-           isSome (assoc (#3 (valOf (assoc (descr, index))), s)))
+           AList.defined (op =) ((#3 o the o AList.lookup (op =) descr) index) s)
              (Symtab.dest (DatatypePackage.get_datatypes thy)) of
           NONE => NONE
         | SOME (tname, {index, descr, ...}) =>
            if isSome (get_assoc_code thy s T) then NONE else
-           let val SOME (_, _, constrs) = assoc (descr, index)
-           in (case (assoc (constrs, s), strip_type T) of
+           let val SOME (_, _, constrs) = AList.lookup (op =) descr index
+           in (case (AList.lookup (op =) constrs s, strip_type T) of
                (NONE, _) => SOME (pretty_case thy defs gr dep module brack
-                 (#3 (valOf (assoc (descr, index)))) c ts)
+                 (#3 (valOf (AList.lookup (op =) descr index))) c ts)
              | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
                  (fst (invoke_tycodegen thy defs dep module false
                     (gr, snd (strip_type T))))
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -112,7 +112,7 @@
 
 fun constrs_of thy tname = (case datatype_info thy tname of
    SOME {index, descr, ...} =>
-     let val (_, _, constrs) = valOf (assoc (descr, index))
+     let val (_, _, constrs) = valOf (AList.lookup (op =) descr index)
      in SOME (map (fn (cname, _) => Const (cname, Sign.the_const_type thy cname)) constrs)
      end
  | _ => NONE);
@@ -126,7 +126,7 @@
 fun find_tname var Bi =
   let val frees = map dest_Free (term_frees Bi)
       val params = rename_wrt_term Bi (Logic.strip_params Bi);
-  in case assoc (frees @ params, var) of
+  in case AList.lookup (op =) (frees @ params) var of
        NONE => error ("No such variable in subgoal: " ^ quote var)
      | SOME(Type (tn, _)) => tn
      | _ => error ("Cannot determine type of " ^ quote var)
@@ -139,7 +139,7 @@
     val params = Logic.strip_params Bi;   (*params of subgoal i*)
     val params = rev (rename_wrt_term Bi params);   (*as they are printed*)
     val (types, sorts) = types_sorts state;
-    fun types' (a, ~1) = (case assoc (params, a) of NONE => types(a, ~1) | sm => sm)
+    fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
       | types' ixn = types ixn;
     val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
   in case #T (rep_cterm ct) of
@@ -261,7 +261,7 @@
 
 fun dt_cases (descr: descr) (_, args, constrs) =
   let
-    fun the_bname i = Sign.base_name (#1 (valOf (assoc (descr, i))));
+    fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
   in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
 
@@ -269,7 +269,7 @@
 fun induct_cases descr =
   DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
 
-fun exhaust_cases descr i = dt_cases descr (valOf (assoc (descr, i)));
+fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
 
 in
 
@@ -456,7 +456,7 @@
        strip_abs (length dts) t, is_dependent (length dts) t))
       (constrs ~~ fs);
     fun count_cases (cs, (_, _, true)) = cs
-      | count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of
+      | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
           NONE => (body, [cname]) :: cs
         | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
     val cases' = sort (int_ord o Library.swap o pairself (length o snd))
@@ -489,7 +489,7 @@
 
 fun read_typ sign ((Ts, sorts), str) =
   let
-    val T = Type.no_tvars (Sign.read_typ (sign, (curry assoc)
+    val T = Type.no_tvars (Sign.read_typ (sign, AList.lookup (op =)
       (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
   in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
 
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -44,7 +44,7 @@
 fun indexify_names names =
   let
     fun index (x :: xs) tab =
-      (case assoc (tab, x) of
+      (case AList.lookup (op =) tab x of
         NONE => if x mem xs then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
       | SOME i => (x ^ Library.string_of_int i) :: index xs ((x, i + 1) :: tab))
     | index [] _ = [];
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -141,7 +141,7 @@
     val rvs = Drule.vars_of_terms [prop_of thm'];
     val ivs1 = map Var (filter_out (fn (_, T) =>
       tname_of (body_type T) mem ["set", "bool"]) ivs);
-    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
+    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
 
     val prf = foldr forall_intr_prf
      (foldr (fn ((f, p), prf) =>
@@ -182,7 +182,7 @@
             list_comb (r, free_ts)))))
       end;
 
-    val SOME (_, _, constrs) = assoc (descr, index);
+    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
     val T = List.nth (get_rec_types descr sorts, index);
     val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
     val r = Const (case_name, map fastype_of rs ---> T --> rT);
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -79,7 +79,7 @@
       else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
     val arities = get_arities descr' \ 0;
     val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
-    val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
+    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
     val oldTs = Library.drop (length (hd descr), recTs);
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -124,15 +124,15 @@
   let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
   in (case (optf, strip_comb t) of
       (SOME f, (Const (name, _), args)) =>
-        (case assoc (extra_fs, name) of
-           NONE => overwrite (fs, (name, getOpt
-             (Option.map (mg_factor f) (assoc (fs, name)), f)))
+        (case AList.lookup (op =) extra_fs name of
+           NONE => AList.update (op =) (name, getOpt
+             (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
          | SOME (fs', f') => (mg_factor f (FFix f');
              Library.foldl (infer_factors sg extra_fs)
                (fs, map (Option.map FFix) fs' ~~ args)))
     | (SOME f, (Var ((name, _), _), [])) =>
-        overwrite (fs, (name, getOpt
-          (Option.map (mg_factor f) (assoc (fs, name)), f)))
+        AList.update (op =) (name, getOpt
+          (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
     | (NONE, _) => fs
     | _ => err "Illegal term")
       handle Factors => err "Product factor mismatch in"
@@ -152,7 +152,7 @@
       (Symtab.dest (DatatypePackage.get_datatypes thy))));
     fun check t = (case strip_comb t of
         (Var _, []) => true
-      | (Const (s, _), ts) => (case assoc (cnstrs, s) of
+      | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
             NONE => false
           | SOME i => length ts = i andalso forall check ts)
       | _ => false)
@@ -209,7 +209,7 @@
         (fn (NONE, _) => [NONE]
           | (SOME js, arg) => map SOME
               (List.filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
-                (iss ~~ args)))) (valOf (assoc (modes, name))))
+                (iss ~~ args)))) ((the o AList.lookup (op =) modes) name))
 
   in (case strip_comb t of
       (Const ("op =", Type (_, [T, _])), _) =>
@@ -230,7 +230,7 @@
             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
             val vTs = List.concat (map term_vTs out_ts');
             val dupTs = map snd (duplicates vTs) @
-              List.mapPartial (curry assoc vTs) vs;
+              List.mapPartial (AList.lookup (op =) vTs) vs;
           in
             terms_vs (in_ts @ in_ts') subset vs andalso
             forall (is_eqT o fastype_of) in_ts' andalso
@@ -264,7 +264,7 @@
   end;
 
 fun check_modes_pred thy arg_vs preds modes (p, ms) =
-  let val SOME rs = assoc (preds, p)
+  let val SOME rs = AList.lookup (op =) preds p
   in (p, List.filter (fn m => case find_index
     (not o check_mode_clause thy arg_vs modes m) rs of
       ~1 => true
@@ -339,10 +339,10 @@
     else ps
   end;
 
-fun mk_v ((names, vs), s) = (case assoc (vs, s) of
+fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
       NONE => ((names, (s, [s])::vs), s)
     | SOME xs => let val s' = variant names s in
-        ((s'::names, overwrite (vs, (s, s'::xs))), s') end);
+        ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
 
 fun distinct_v (nvs, Var ((s, 0), T)) =
       apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s))
@@ -417,7 +417,7 @@
       foldl_map check_constrt ((all_vs, []), in_ts);
 
     fun is_ind t = (case head_of t of
-          Const (s, _) => s = "op =" orelse isSome (assoc (modes, s))
+          Const (s, _) => s = "op =" orelse AList.defined (op =) modes s
         | Var ((s, _), _) => s mem arg_vs);
 
     fun compile_prems out_ts' vs names gr [] =
@@ -508,7 +508,7 @@
   let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
     foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
       dep module prfx' all_vs arg_vs modes s cls mode)
-        ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
+        ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
   in
     (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
   end;
@@ -532,7 +532,7 @@
 fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
 
 fun constrain cs [] = []
-  | constrain cs ((s, xs) :: ys) = (s, case assoc (cs, s) of
+  | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs s of
       NONE => xs
     | SOME xs' => xs inter xs') :: constrain cs ys;
 
@@ -554,7 +554,7 @@
       val arg_vs = List.concat (map term_vs args);
 
       fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
-            (case assoc (factors, case head_of u of
+            (case AList.lookup (op =) factors (case head_of u of
                  Const (name, _) => name | Var ((name, _), _) => name) of
                NONE => Prem (full_split_prod t, u)
              | SOME f => Prem (split_prod [] f t, u))
@@ -568,8 +568,8 @@
           val Const (name, _) = head_of u;
           val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
         in
-          (overwrite (clauses, (name, getOpt (assoc (clauses, name), []) @
-             [(split_prod [] (valOf (assoc (factors, name))) t, prems)])))
+          AList.update (op =) (name, ((these o AList.lookup (op =) clauses) name) @
+             [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
         end;
 
       fun check_set (Const (s, _)) = s mem names orelse isSome (get_clauses thy s)
@@ -592,7 +592,7 @@
           Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
       val factors = List.mapPartial (fn (name, f) =>
         if name mem arg_vs then NONE
-        else SOME (name, (map (curry assoc fs) arg_vs, f))) fs;
+        else SOME (name, (map (AList.lookup (op =) fs) arg_vs, f))) fs;
       val clauses =
         Library.foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
       val modes = constrain modecs
@@ -626,7 +626,7 @@
              (mk_ind_def thy defs gr dep names module'
              [] [] (prep_intrs intrs)) dep names module' [u];
            val (modes, factors) = lookup_modes gr1 dep;
-           val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
+           val ts = split_prod [] ((snd o the o AList.lookup (op =) factors) s) t;
            val (ts', is) = if is_query then
                fst (Library.foldl mk_mode ((([], []), 1), ts))
              else (ts, 1 upto length ts);
@@ -659,7 +659,7 @@
            SOME (gr2, (if brack then parens else I)
              (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
                Pretty.str "("] @
-               conv_ntuple' (snd (valOf (assoc (factors, s))))
+                conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))
                  (HOLogic.dest_setT (fastype_of u))
                  (ps @ [Pretty.brk 1, Pretty.str "()"]) @
                [Pretty.str ")"])))
diff -r 8581c151adea -r 0f1c48de39f5 src/HOL/eqrule_HOL_data.ML
--- a/src/HOL/eqrule_HOL_data.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/eqrule_HOL_data.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -45,8 +45,8 @@
            Const("Trueprop",_) $ p =>
              (case Term.head_of p of
                 Const(a,_) =>
-                  (case Library.assoc(pairs,a) of
-                     SOME(rls) => List.concat (map atoms ([th] RL rls))
+                  (case AList.lookup (op =) pairs a of
+                     SOME rls => List.concat (map atoms ([th] RL rls))
                    | NONE => [th])
               | _ => [th])
          | _ => [th])
diff -r 8581c151adea -r 0f1c48de39f5 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/Pure/General/output.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -160,10 +160,13 @@
   in asl l end;
 
 fun overwrite_warn (args as (alist, (a, _))) msg =
- (if is_none (assoc (alist, a)) then () else warning msg;
+ (if is_none (AList.lookup (op =) alist a) then () else warning msg;
   overwrite args);
 
-
+fun update_warn eq msg (kv as (key, value)) xs = (
+  if (not o AList.defined eq xs) key then () else warning msg;
+  AList.update eq kv xs
+)
 
 (** handle errors  **)
 
diff -r 8581c151adea -r 0f1c48de39f5 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Sep 20 15:12:40 2005 +0200
+++ b/src/Pure/codegen.ML	Tue Sep 20 16:17:34 2005 +0200
@@ -267,7 +267,7 @@
 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,
@@ -278,7 +278,7 @@
 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,
@@ -292,7 +292,7 @@
 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,
@@ -358,7 +358,7 @@
                   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,
@@ -381,7 +381,7 @@
       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,
@@ -389,7 +389,7 @@
      | 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 ****)
@@ -514,7 +514,7 @@
     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)
@@ -748,7 +748,7 @@
   | 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
@@ -779,8 +779,7 @@
 
 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
@@ -954,8 +953,8 @@
     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" ^
@@ -1075,7 +1074,7 @@
    ("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 =>