introduced AList module in favor of assoc etc.
authorhaftmann
Tue Sep 20 16:17:34 2005 +0200 (2005-09-20)
changeset 175210f1c48de39f5
parent 17520 8581c151adea
child 17522 8d25bb07d8ed
introduced AList module in favor of assoc etc.
src/FOL/eqrule_FOL_data.ML
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/reflected_cooper.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/reflected_cooper.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/eqrule_HOL_data.ML
src/Pure/General/output.ML
src/Pure/codegen.ML
     1.1 --- a/src/FOL/eqrule_FOL_data.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/FOL/eqrule_FOL_data.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -36,8 +36,8 @@
     1.4             Const("Trueprop",_) $ p =>
     1.5               (case Term.head_of p of
     1.6                  Const(a,_) =>
     1.7 -                  (case Library.assoc(pairs,a) of
     1.8 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
     1.9 +                  (case AList.lookup (op =) pairs a of
    1.10 +                     SOME rls => List.concat (map atoms ([th] RL rls))
    1.11                     | NONE => [th])
    1.12                | _ => [th])
    1.13           | _ => [th])
     2.1 --- a/src/HOL/Integ/cooper_dec.ML	Tue Sep 20 15:12:40 2005 +0200
     2.2 +++ b/src/HOL/Integ/cooper_dec.ML	Tue Sep 20 16:17:34 2005 +0200
     2.3 @@ -467,12 +467,12 @@
     2.4       else HOLogic.false_const)
     2.5        handle _ => at)
     2.6      else
     2.7 -  case assoc (operations,p) of 
     2.8 +  case AList.lookup (op =) operations p of 
     2.9      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    2.10      handle _ => at) 
    2.11        | _ =>  at) 
    2.12        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    2.13 -  case assoc (operations,p) of 
    2.14 +  case AList.lookup (op =) operations p of 
    2.15      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    2.16      HOLogic.false_const else HOLogic.true_const)  
    2.17      handle _ => at) 
     3.1 --- a/src/HOL/Integ/reflected_cooper.ML	Tue Sep 20 15:12:40 2005 +0200
     3.2 +++ b/src/HOL/Integ/reflected_cooper.ML	Tue Sep 20 16:17:34 2005 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  fun i_of_term vs t = 
     3.6      case t of
     3.7 -	Free(xn,xT) => (case assoc(vs,t) of 
     3.8 +	Free(xn,xT) => (case AList.lookup (op =) vs t of 
     3.9  			   NONE   => error "Variable not found in the list!!"
    3.10  			 | SOME n => Var n)
    3.11        | Const("0",iT) => Cst 0
     4.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 20 15:12:40 2005 +0200
     4.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 20 16:17:34 2005 +0200
     4.3 @@ -969,10 +969,10 @@
     4.4  	val header = readHeader () 
     4.5  
     4.6  	val result = 
     4.7 -	    case assoc (header, "STATUS") of
     4.8 +	    case AList.lookup (op =) header "STATUS" of
     4.9  		SOME "INFEASIBLE" => Infeasible
    4.10  	      | SOME "UNBOUNDED" => Unbounded
    4.11 -	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
    4.12 +	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
    4.13  					   (skip_until_sep (); 
    4.14  					    skip_until_sep ();
    4.15  					    load_values ()))
    4.16 @@ -1118,10 +1118,10 @@
    4.17  	val header = readHeader ()
    4.18  
    4.19  	val result = 
    4.20 -	    case assoc (header, "STATUS") of
    4.21 +	    case AList.lookup (op =) header "STATUS" of
    4.22  		SOME "INFEASIBLE" => Infeasible
    4.23  	      | SOME "NONOPTIMAL" => Unbounded
    4.24 -	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
    4.25 +	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
    4.26  					   (skip_paragraph (); 
    4.27  					    skip_paragraph (); 
    4.28  					    skip_paragraph (); 
     5.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Sep 20 15:12:40 2005 +0200
     5.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Sep 20 16:17:34 2005 +0200
     5.3 @@ -467,12 +467,12 @@
     5.4       else HOLogic.false_const)
     5.5        handle _ => at)
     5.6      else
     5.7 -  case assoc (operations,p) of 
     5.8 +  case AList.lookup (op =) operations p of 
     5.9      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    5.10      handle _ => at) 
    5.11        | _ =>  at) 
    5.12        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    5.13 -  case assoc (operations,p) of 
    5.14 +  case AList.lookup (op =) operations p of 
    5.15      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    5.16      HOLogic.false_const else HOLogic.true_const)  
    5.17      handle _ => at) 
     6.1 --- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Tue Sep 20 15:12:40 2005 +0200
     6.2 +++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Tue Sep 20 16:17:34 2005 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  
     6.5  fun i_of_term vs t = 
     6.6      case t of
     6.7 -	Free(xn,xT) => (case assoc(vs,t) of 
     6.8 +	Free(xn,xT) => (case AList.lookup (op =) vs t of 
     6.9  			   NONE   => error "Variable not found in the list!!"
    6.10  			 | SOME n => Var n)
    6.11        | Const("0",iT) => Cst 0
     7.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 20 15:12:40 2005 +0200
     7.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 20 16:17:34 2005 +0200
     7.3 @@ -26,7 +26,7 @@
     7.4  
     7.5  fun find_nonempty (descr: DatatypeAux.descr) is i =
     7.6    let
     7.7 -    val (_, _, constrs) = valOf (assoc (descr, i));
     7.8 +    val (_, _, constrs) = valOf (AList.lookup (op =) descr i);
     7.9      fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE
    7.10            else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
    7.11        | arg_nonempty _ = SOME 0;
    7.12 @@ -160,7 +160,7 @@
    7.13                   [Pretty.block [Pretty.str "(case", Pretty.brk 1,
    7.14                     Pretty.str "i", Pretty.brk 1, Pretty.str "of",
    7.15                     Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
    7.16 -                   mk_constr "0" true (cname, valOf (assoc (cs, cname))),
    7.17 +                   mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
    7.18                     Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
    7.19                     mk_choice cs1, Pretty.str ")"]]
    7.20                 else [mk_choice cs2])) ::
    7.21 @@ -263,15 +263,15 @@
    7.22     (c as Const (s, T), ts) =>
    7.23         (case find_first (fn (_, {index, descr, case_name, ...}) =>
    7.24           s = case_name orelse
    7.25 -           isSome (assoc (#3 (valOf (assoc (descr, index))), s)))
    7.26 +           AList.defined (op =) ((#3 o the o AList.lookup (op =) descr) index) s)
    7.27               (Symtab.dest (DatatypePackage.get_datatypes thy)) of
    7.28            NONE => NONE
    7.29          | SOME (tname, {index, descr, ...}) =>
    7.30             if isSome (get_assoc_code thy s T) then NONE else
    7.31 -           let val SOME (_, _, constrs) = assoc (descr, index)
    7.32 -           in (case (assoc (constrs, s), strip_type T) of
    7.33 +           let val SOME (_, _, constrs) = AList.lookup (op =) descr index
    7.34 +           in (case (AList.lookup (op =) constrs s, strip_type T) of
    7.35                 (NONE, _) => SOME (pretty_case thy defs gr dep module brack
    7.36 -                 (#3 (valOf (assoc (descr, index)))) c ts)
    7.37 +                 (#3 (valOf (AList.lookup (op =) descr index))) c ts)
    7.38               | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
    7.39                   (fst (invoke_tycodegen thy defs dep module false
    7.40                      (gr, snd (strip_type T))))
     8.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 20 15:12:40 2005 +0200
     8.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 20 16:17:34 2005 +0200
     8.3 @@ -112,7 +112,7 @@
     8.4  
     8.5  fun constrs_of thy tname = (case datatype_info thy tname of
     8.6     SOME {index, descr, ...} =>
     8.7 -     let val (_, _, constrs) = valOf (assoc (descr, index))
     8.8 +     let val (_, _, constrs) = valOf (AList.lookup (op =) descr index)
     8.9       in SOME (map (fn (cname, _) => Const (cname, Sign.the_const_type thy cname)) constrs)
    8.10       end
    8.11   | _ => NONE);
    8.12 @@ -126,7 +126,7 @@
    8.13  fun find_tname var Bi =
    8.14    let val frees = map dest_Free (term_frees Bi)
    8.15        val params = rename_wrt_term Bi (Logic.strip_params Bi);
    8.16 -  in case assoc (frees @ params, var) of
    8.17 +  in case AList.lookup (op =) (frees @ params) var of
    8.18         NONE => error ("No such variable in subgoal: " ^ quote var)
    8.19       | SOME(Type (tn, _)) => tn
    8.20       | _ => error ("Cannot determine type of " ^ quote var)
    8.21 @@ -139,7 +139,7 @@
    8.22      val params = Logic.strip_params Bi;   (*params of subgoal i*)
    8.23      val params = rev (rename_wrt_term Bi params);   (*as they are printed*)
    8.24      val (types, sorts) = types_sorts state;
    8.25 -    fun types' (a, ~1) = (case assoc (params, a) of NONE => types(a, ~1) | sm => sm)
    8.26 +    fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
    8.27        | types' ixn = types ixn;
    8.28      val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
    8.29    in case #T (rep_cterm ct) of
    8.30 @@ -261,7 +261,7 @@
    8.31  
    8.32  fun dt_cases (descr: descr) (_, args, constrs) =
    8.33    let
    8.34 -    fun the_bname i = Sign.base_name (#1 (valOf (assoc (descr, i))));
    8.35 +    fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
    8.36      val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
    8.37    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    8.38  
    8.39 @@ -269,7 +269,7 @@
    8.40  fun induct_cases descr =
    8.41    DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    8.42  
    8.43 -fun exhaust_cases descr i = dt_cases descr (valOf (assoc (descr, i)));
    8.44 +fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    8.45  
    8.46  in
    8.47  
    8.48 @@ -456,7 +456,7 @@
    8.49         strip_abs (length dts) t, is_dependent (length dts) t))
    8.50        (constrs ~~ fs);
    8.51      fun count_cases (cs, (_, _, true)) = cs
    8.52 -      | count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of
    8.53 +      | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
    8.54            NONE => (body, [cname]) :: cs
    8.55          | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
    8.56      val cases' = sort (int_ord o Library.swap o pairself (length o snd))
    8.57 @@ -489,7 +489,7 @@
    8.58  
    8.59  fun read_typ sign ((Ts, sorts), str) =
    8.60    let
    8.61 -    val T = Type.no_tvars (Sign.read_typ (sign, (curry assoc)
    8.62 +    val T = Type.no_tvars (Sign.read_typ (sign, AList.lookup (op =)
    8.63        (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
    8.64    in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
    8.65  
     9.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Sep 20 15:12:40 2005 +0200
     9.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Sep 20 16:17:34 2005 +0200
     9.3 @@ -44,7 +44,7 @@
     9.4  fun indexify_names names =
     9.5    let
     9.6      fun index (x :: xs) tab =
     9.7 -      (case assoc (tab, x) of
     9.8 +      (case AList.lookup (op =) tab x of
     9.9          NONE => if x mem xs then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
    9.10        | SOME i => (x ^ Library.string_of_int i) :: index xs ((x, i + 1) :: tab))
    9.11      | index [] _ = [];
    10.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 20 15:12:40 2005 +0200
    10.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 20 16:17:34 2005 +0200
    10.3 @@ -141,7 +141,7 @@
    10.4      val rvs = Drule.vars_of_terms [prop_of thm'];
    10.5      val ivs1 = map Var (filter_out (fn (_, T) =>
    10.6        tname_of (body_type T) mem ["set", "bool"]) ivs);
    10.7 -    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
    10.8 +    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
    10.9  
   10.10      val prf = foldr forall_intr_prf
   10.11       (foldr (fn ((f, p), prf) =>
   10.12 @@ -182,7 +182,7 @@
   10.13              list_comb (r, free_ts)))))
   10.14        end;
   10.15  
   10.16 -    val SOME (_, _, constrs) = assoc (descr, index);
   10.17 +    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
   10.18      val T = List.nth (get_rec_types descr sorts, index);
   10.19      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
   10.20      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    11.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 20 15:12:40 2005 +0200
    11.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 20 16:17:34 2005 +0200
    11.3 @@ -79,7 +79,7 @@
    11.4        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
    11.5      val arities = get_arities descr' \ 0;
    11.6      val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
    11.7 -    val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
    11.8 +    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
    11.9      val recTs = get_rec_types descr' sorts;
   11.10      val newTs = Library.take (length (hd descr), recTs);
   11.11      val oldTs = Library.drop (length (hd descr), recTs);
    12.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Sep 20 15:12:40 2005 +0200
    12.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Sep 20 16:17:34 2005 +0200
    12.3 @@ -124,15 +124,15 @@
    12.4    let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
    12.5    in (case (optf, strip_comb t) of
    12.6        (SOME f, (Const (name, _), args)) =>
    12.7 -        (case assoc (extra_fs, name) of
    12.8 -           NONE => overwrite (fs, (name, getOpt
    12.9 -             (Option.map (mg_factor f) (assoc (fs, name)), f)))
   12.10 +        (case AList.lookup (op =) extra_fs name of
   12.11 +           NONE => AList.update (op =) (name, getOpt
   12.12 +             (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
   12.13           | SOME (fs', f') => (mg_factor f (FFix f');
   12.14               Library.foldl (infer_factors sg extra_fs)
   12.15                 (fs, map (Option.map FFix) fs' ~~ args)))
   12.16      | (SOME f, (Var ((name, _), _), [])) =>
   12.17 -        overwrite (fs, (name, getOpt
   12.18 -          (Option.map (mg_factor f) (assoc (fs, name)), f)))
   12.19 +        AList.update (op =) (name, getOpt
   12.20 +          (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
   12.21      | (NONE, _) => fs
   12.22      | _ => err "Illegal term")
   12.23        handle Factors => err "Product factor mismatch in"
   12.24 @@ -152,7 +152,7 @@
   12.25        (Symtab.dest (DatatypePackage.get_datatypes thy))));
   12.26      fun check t = (case strip_comb t of
   12.27          (Var _, []) => true
   12.28 -      | (Const (s, _), ts) => (case assoc (cnstrs, s) of
   12.29 +      | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
   12.30              NONE => false
   12.31            | SOME i => length ts = i andalso forall check ts)
   12.32        | _ => false)
   12.33 @@ -209,7 +209,7 @@
   12.34          (fn (NONE, _) => [NONE]
   12.35            | (SOME js, arg) => map SOME
   12.36                (List.filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
   12.37 -                (iss ~~ args)))) (valOf (assoc (modes, name))))
   12.38 +                (iss ~~ args)))) ((the o AList.lookup (op =) modes) name))
   12.39  
   12.40    in (case strip_comb t of
   12.41        (Const ("op =", Type (_, [T, _])), _) =>
   12.42 @@ -230,7 +230,7 @@
   12.43              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
   12.44              val vTs = List.concat (map term_vTs out_ts');
   12.45              val dupTs = map snd (duplicates vTs) @
   12.46 -              List.mapPartial (curry assoc vTs) vs;
   12.47 +              List.mapPartial (AList.lookup (op =) vTs) vs;
   12.48            in
   12.49              terms_vs (in_ts @ in_ts') subset vs andalso
   12.50              forall (is_eqT o fastype_of) in_ts' andalso
   12.51 @@ -264,7 +264,7 @@
   12.52    end;
   12.53  
   12.54  fun check_modes_pred thy arg_vs preds modes (p, ms) =
   12.55 -  let val SOME rs = assoc (preds, p)
   12.56 +  let val SOME rs = AList.lookup (op =) preds p
   12.57    in (p, List.filter (fn m => case find_index
   12.58      (not o check_mode_clause thy arg_vs modes m) rs of
   12.59        ~1 => true
   12.60 @@ -339,10 +339,10 @@
   12.61      else ps
   12.62    end;
   12.63  
   12.64 -fun mk_v ((names, vs), s) = (case assoc (vs, s) of
   12.65 +fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
   12.66        NONE => ((names, (s, [s])::vs), s)
   12.67      | SOME xs => let val s' = variant names s in
   12.68 -        ((s'::names, overwrite (vs, (s, s'::xs))), s') end);
   12.69 +        ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
   12.70  
   12.71  fun distinct_v (nvs, Var ((s, 0), T)) =
   12.72        apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s))
   12.73 @@ -417,7 +417,7 @@
   12.74        foldl_map check_constrt ((all_vs, []), in_ts);
   12.75  
   12.76      fun is_ind t = (case head_of t of
   12.77 -          Const (s, _) => s = "op =" orelse isSome (assoc (modes, s))
   12.78 +          Const (s, _) => s = "op =" orelse AList.defined (op =) modes s
   12.79          | Var ((s, _), _) => s mem arg_vs);
   12.80  
   12.81      fun compile_prems out_ts' vs names gr [] =
   12.82 @@ -508,7 +508,7 @@
   12.83    let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
   12.84      foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
   12.85        dep module prfx' all_vs arg_vs modes s cls mode)
   12.86 -        ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
   12.87 +        ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
   12.88    in
   12.89      (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
   12.90    end;
   12.91 @@ -532,7 +532,7 @@
   12.92  fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
   12.93  
   12.94  fun constrain cs [] = []
   12.95 -  | constrain cs ((s, xs) :: ys) = (s, case assoc (cs, s) of
   12.96 +  | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs s of
   12.97        NONE => xs
   12.98      | SOME xs' => xs inter xs') :: constrain cs ys;
   12.99  
  12.100 @@ -554,7 +554,7 @@
  12.101        val arg_vs = List.concat (map term_vs args);
  12.102  
  12.103        fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
  12.104 -            (case assoc (factors, case head_of u of
  12.105 +            (case AList.lookup (op =) factors (case head_of u of
  12.106                   Const (name, _) => name | Var ((name, _), _) => name) of
  12.107                 NONE => Prem (full_split_prod t, u)
  12.108               | SOME f => Prem (split_prod [] f t, u))
  12.109 @@ -568,8 +568,8 @@
  12.110            val Const (name, _) = head_of u;
  12.111            val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
  12.112          in
  12.113 -          (overwrite (clauses, (name, getOpt (assoc (clauses, name), []) @
  12.114 -             [(split_prod [] (valOf (assoc (factors, name))) t, prems)])))
  12.115 +          AList.update (op =) (name, ((these o AList.lookup (op =) clauses) name) @
  12.116 +             [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
  12.117          end;
  12.118  
  12.119        fun check_set (Const (s, _)) = s mem names orelse isSome (get_clauses thy s)
  12.120 @@ -592,7 +592,7 @@
  12.121            Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
  12.122        val factors = List.mapPartial (fn (name, f) =>
  12.123          if name mem arg_vs then NONE
  12.124 -        else SOME (name, (map (curry assoc fs) arg_vs, f))) fs;
  12.125 +        else SOME (name, (map (AList.lookup (op =) fs) arg_vs, f))) fs;
  12.126        val clauses =
  12.127          Library.foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
  12.128        val modes = constrain modecs
  12.129 @@ -626,7 +626,7 @@
  12.130               (mk_ind_def thy defs gr dep names module'
  12.131               [] [] (prep_intrs intrs)) dep names module' [u];
  12.132             val (modes, factors) = lookup_modes gr1 dep;
  12.133 -           val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
  12.134 +           val ts = split_prod [] ((snd o the o AList.lookup (op =) factors) s) t;
  12.135             val (ts', is) = if is_query then
  12.136                 fst (Library.foldl mk_mode ((([], []), 1), ts))
  12.137               else (ts, 1 upto length ts);
  12.138 @@ -659,7 +659,7 @@
  12.139             SOME (gr2, (if brack then parens else I)
  12.140               (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
  12.141                 Pretty.str "("] @
  12.142 -               conv_ntuple' (snd (valOf (assoc (factors, s))))
  12.143 +                conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))
  12.144                   (HOLogic.dest_setT (fastype_of u))
  12.145                   (ps @ [Pretty.brk 1, Pretty.str "()"]) @
  12.146                 [Pretty.str ")"])))
    13.1 --- a/src/HOL/eqrule_HOL_data.ML	Tue Sep 20 15:12:40 2005 +0200
    13.2 +++ b/src/HOL/eqrule_HOL_data.ML	Tue Sep 20 16:17:34 2005 +0200
    13.3 @@ -45,8 +45,8 @@
    13.4             Const("Trueprop",_) $ p =>
    13.5               (case Term.head_of p of
    13.6                  Const(a,_) =>
    13.7 -                  (case Library.assoc(pairs,a) of
    13.8 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
    13.9 +                  (case AList.lookup (op =) pairs a of
   13.10 +                     SOME rls => List.concat (map atoms ([th] RL rls))
   13.11                     | NONE => [th])
   13.12                | _ => [th])
   13.13           | _ => [th])
    14.1 --- a/src/Pure/General/output.ML	Tue Sep 20 15:12:40 2005 +0200
    14.2 +++ b/src/Pure/General/output.ML	Tue Sep 20 16:17:34 2005 +0200
    14.3 @@ -160,10 +160,13 @@
    14.4    in asl l end;
    14.5  
    14.6  fun overwrite_warn (args as (alist, (a, _))) msg =
    14.7 - (if is_none (assoc (alist, a)) then () else warning msg;
    14.8 + (if is_none (AList.lookup (op =) alist a) then () else warning msg;
    14.9    overwrite args);
   14.10  
   14.11 -
   14.12 +fun update_warn eq msg (kv as (key, value)) xs = (
   14.13 +  if (not o AList.defined eq xs) key then () else warning msg;
   14.14 +  AList.update eq kv xs
   14.15 +)
   14.16  
   14.17  (** handle errors  **)
   14.18  
    15.1 --- a/src/Pure/codegen.ML	Tue Sep 20 15:12:40 2005 +0200
    15.2 +++ b/src/Pure/codegen.ML	Tue Sep 20 16:17:34 2005 +0200
    15.3 @@ -267,7 +267,7 @@
    15.4  fun add_codegen name f thy =
    15.5    let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    15.6      CodegenData.get thy
    15.7 -  in (case assoc (codegens, name) of
    15.8 +  in (case AList.lookup (op =) codegens name of
    15.9        NONE => CodegenData.put {codegens = (name, f) :: codegens,
   15.10          tycodegens = tycodegens, consts = consts, types = types,
   15.11          attrs = attrs, preprocs = preprocs, modules = modules,
   15.12 @@ -278,7 +278,7 @@
   15.13  fun add_tycodegen name f thy =
   15.14    let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   15.15      CodegenData.get thy
   15.16 -  in (case assoc (tycodegens, name) of
   15.17 +  in (case AList.lookup (op =) tycodegens name of
   15.18        NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
   15.19          codegens = codegens, consts = consts, types = types,
   15.20          attrs = attrs, preprocs = preprocs, modules = modules,
   15.21 @@ -292,7 +292,7 @@
   15.22  fun add_attribute name att thy =
   15.23    let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   15.24      CodegenData.get thy
   15.25 -  in (case assoc (attrs, name) of
   15.26 +  in (case AList.lookup (op =) attrs name of
   15.27        NONE => CodegenData.put {tycodegens = tycodegens,
   15.28          codegens = codegens, consts = consts, types = types,
   15.29          attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
   15.30 @@ -358,7 +358,7 @@
   15.31                    in if Sign.typ_instance thy (U, T) then U
   15.32                      else error ("Illegal type constraint for constant " ^ cname)
   15.33                    end)
   15.34 -         in (case assoc (consts, (cname, T')) of
   15.35 +         in (case AList.lookup (op =) consts (cname, T') of
   15.36               NONE => CodegenData.put {codegens = codegens,
   15.37                 tycodegens = tycodegens,
   15.38                 consts = ((cname, T'), syn) :: consts,
   15.39 @@ -381,7 +381,7 @@
   15.40        CodegenData.get thy;
   15.41      val tc = Sign.intern_type thy s
   15.42    in
   15.43 -    (case assoc (types, tc) of
   15.44 +    (case AList.lookup (op =) types tc of
   15.45         NONE => CodegenData.put {codegens = codegens,
   15.46           tycodegens = tycodegens, consts = consts,
   15.47           types = (tc, syn) :: types, attrs = attrs,
   15.48 @@ -389,7 +389,7 @@
   15.49       | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   15.50    end) (thy, xs);
   15.51  
   15.52 -fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s);
   15.53 +fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
   15.54  
   15.55  
   15.56  (**** make valid ML identifiers ****)
   15.57 @@ -514,7 +514,7 @@
   15.58      val ps = (reserved @ illegal) ~~
   15.59        variantlist (map (suffix "'") reserved @ alt_names, names);
   15.60  
   15.61 -    fun rename_id s = getOpt (assoc (ps, s), s);
   15.62 +    fun rename_id s = AList.lookup (op =) ps s |> the_default s;
   15.63  
   15.64      fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
   15.65        | rename (Free (a, T)) = Free (rename_id a, T)
   15.66 @@ -748,7 +748,7 @@
   15.67    | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
   15.68        SOME (gr, Pretty.str s)
   15.69    | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   15.70 -      (case assoc (#types (CodegenData.get thy), s) of
   15.71 +      (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
   15.72           NONE => NONE
   15.73         | SOME (ms, aux) =>
   15.74             let
   15.75 @@ -779,8 +779,7 @@
   15.76  
   15.77  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
   15.78  
   15.79 -fun add_to_module name s ms =
   15.80 -  overwrite (ms, (name, the (assoc (ms, name)) ^ s));
   15.81 +fun add_to_module name s = AList.map_entry (op =) name (suffix s);
   15.82  
   15.83  fun output_code gr module xs =
   15.84    let
   15.85 @@ -954,8 +953,8 @@
   15.86      val (gi, frees) = Logic.goal_params
   15.87        (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
   15.88      val gi' = ObjectLogic.atomize_term thy (map_term_types
   15.89 -      (map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
   15.90 -        getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
   15.91 +      (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
   15.92 +        getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
   15.93    in case test_term (Toplevel.theory_of st) size iterations gi' of
   15.94        NONE => writeln "No counterexamples found."
   15.95      | SOME cex => writeln ("Counterexample found:\n" ^
   15.96 @@ -1075,7 +1074,7 @@
   15.97     ("default_type", P.typ >> set_default_type)];
   15.98  
   15.99  val parse_test_params = P.short_ident :-- (fn s =>
  15.100 -  P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
  15.101 +  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
  15.102  
  15.103  fun parse_tyinst xs =
  15.104    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>