# HG changeset patch
# User wenzelm
# Date 1125325084 -7200
# Node ID 3d80209e9a5389afdd2f3569b8ad84dad84f8ff5
# Parent  a788a05fb81bad9f289ae705656df4c79b84c731
use AList operations;

diff -r a788a05fb81b -r 3d80209e9a53 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -72,11 +72,11 @@
      (check_vars "repeated variable names in pattern: " (duplicates lfrees);
       check_vars "extra variables on rhs: "
         (map dest_Free (term_frees rhs) \\ lfrees);
-      case assoc (rec_fns, fnameT) of
+      case AList.lookup (op =) rec_fns fnameT of
         NONE =>
           (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
       | SOME (_, rpos', eqns) =>
-          if isSome (assoc (eqns, cname)) then
+          if AList.defined (op =) eqns cname then
             raise RecError "constructor already occurred as pattern"
           else if rpos <> rpos' then
             raise RecError "position of recursive argument inconsistent"
@@ -104,7 +104,7 @@
             if is_Const f andalso dest_Const f mem map fst rec_eqns then
               let
                 val fnameT' as (fname', _) = dest_Const f;
-                val (_, rpos, _) = valOf (assoc (rec_eqns, fnameT'));
+                val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
                 val ls = Library.take (rpos, ts);
                 val rest = Library.drop (rpos, ts);
                 val (x', rs) = (hd rest, tl rest)
@@ -112,7 +112,7 @@
                    \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
                 val (x, xs) = strip_comb x'
               in 
-                (case assoc (subs, x) of
+                (case AList.lookup (op =) subs x of
                     NONE =>
                       let
                         val (fs', ts') = foldl_map (subst subs) (fs, ts)
@@ -134,7 +134,7 @@
     (* translate rec equations into function arguments suitable for rec comb *)
 
     fun trans eqns ((cname, cargs), (fnameTs', fnss', fns)) =
-      (case assoc (eqns, cname) of
+      (case AList.lookup (op =) eqns cname of
           NONE => (warning ("No equation for constructor " ^ quote cname ^
             "\nin definition of function " ^ quote fname);
               (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
@@ -154,13 +154,13 @@
 		(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
             end)
 
-  in (case assoc (fnameTs, i) of
+  in (case AList.lookup (op =) fnameTs i of
       NONE =>
         if exists (equal fnameT o snd) fnameTs then
           raise RecError ("inconsistent functions for datatype " ^ quote tname)
         else
           let
-            val (_, _, eqns) = valOf (assoc (rec_eqns, fnameT));
+            val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT);
             val (fnameTs', fnss', fns) = foldr (trans eqns)
               ((i, fnameT)::fnameTs, fnss, []) constrs
           in
@@ -175,7 +175,7 @@
 (* prepare functions needed for definitions *)
 
 fun get_fns fns (((i, (tname, _, constrs)), rec_name), (fs, defs)) =
-  case assoc (fns, i) of
+  case AList.lookup (op =) fns i of
      NONE =>
        let
          val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
@@ -216,7 +216,7 @@
   let
     fun constrs_of (_, (_, _, cs)) =
       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
-    val params_of = Library.assocs (List.concat (map constrs_of rec_eqns));
+    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
   in
     induction
     |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
diff -r a788a05fb81b -r 3d80209e9a53 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Provers/splitter.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -240,7 +240,7 @@
                              then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
                              else find tups
                           end
-                in find (assocs cmap c) end
+                in find (these (AList.lookup (op =) cmap c)) end
             | _ => []
           in snd(Library.foldl iter ((0, a), ts)) end
   in posns Ts [] [] t end;
@@ -331,7 +331,7 @@
             (case concl_of thm of _$(t as _$lhs)$_ =>
                (case strip_comb lhs of (Const(a,aT),args) =>
                   let val info = (aT,lhs,thm,fastype_of t,length args)
-                  in case assoc(cmap,a) of
+                  in case AList.lookup (op =) cmap a of
                        SOME infos => overwrite(cmap,(a,info::infos))
                      | NONE => (a,[info])::cmap
                   end
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -338,18 +338,18 @@
     val external_insts''' = xs ~~ ts;
     val term_insts''' = internal_insts''' @ external_insts''';
     val thm''' = instantiate thy inferred external_insts''' thm'';
-  in
+
 
     (* assign internalized values *)
 
-    mixed_insts |> List.app (fn (arg, (xi, _)) =>
-      if is_tvar xi then
-        Args.assign (SOME (Args.Typ (the (assoc (type_insts''', xi))))) arg
-      else
-        Args.assign (SOME (Args.Term (the (assoc (term_insts''', xi))))) arg);
+    val _ =
+      mixed_insts |> List.app (fn (arg, (xi, _)) =>
+        if is_tvar xi then
+          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts''' xi)))) arg
+        else
+          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
 
-    (context, thm''' |> RuleCases.save thm)
-  end;
+  in (context, thm''' |> RuleCases.save thm) end;
 
 end;
 
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -85,7 +85,7 @@
   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
     Drule.eq_thm_prop (th1, th2));
 
-fun lookup_rule (rs: rules) name = assoc_string (NetRules.rules rs, name);
+fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
 
 fun print_rules prt kind x rs =
   let val thms = map snd (NetRules.rules rs)
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -143,7 +143,7 @@
   ("const", (Sign.intern_const, Sign.declared_const, Theory.hide_consts_i))];
 
 fun gen_hide int (kind, xnames) thy =
-  (case assoc_string (kinds, kind) of
+  (case AList.lookup (op =) kinds kind of
     SOME (intern, check, hide) =>
       let
         val names = if int then map (intern thy) xnames else xnames;
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -132,7 +132,7 @@
     SOME (((_, k), _), _) => OuterKeyword.tags_of k
   | NONE => []);
 
-fun is_markup kind name = (assoc_string (! global_markups, name) = SOME kind);
+fun is_markup kind name = (AList.lookup (op =) (! global_markups) name = SOME kind);
 
 
 (* augment syntax *)
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -406,7 +406,7 @@
 
 (* internalize Skolem constants *)
 
-fun lookup_skolem ctxt x = assoc (fixes_of ctxt, x);
+val lookup_skolem = AList.lookup (op =) o fixes_of;
 fun get_skolem ctxt x = if_none (lookup_skolem ctxt x) x;
 
 fun no_skolem internal ctxt x =
@@ -437,7 +437,7 @@
     val rev_fixes = map Library.swap (fixes_of ctxt);
 
     fun extern (t as Free (x, T)) =
-          (case assoc (rev_fixes, x) of
+          (case AList.lookup (op =) rev_fixes x of
             SOME x' => Free (if lookup_skolem ctxt x' = SOME x then x' else NameSpace.hidden x', T)
           | NONE => t)
       | extern (t $ u) = extern t $ extern u
@@ -1259,7 +1259,7 @@
 in
 
 fun get_case ctxt name xs =
-  (case assoc_string (cases_of ctxt, name) of
+  (case AList.lookup (op =) (cases_of ctxt) name of
     NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
   | SOME c => prep_case ctxt name xs c);
 
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -38,7 +38,7 @@
 
 fun lookup_consumes thm =
   let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
-    (case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of
+    (case AList.lookup (op =) (Thm.tags_of_thm thm) (consumes_tagN) of
       NONE => NONE
     | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
     | _ => err ())
@@ -64,7 +64,7 @@
       |> Drule.untag_rule cases_tagN
       |> Drule.tag_rule (cases_tagN, names);
 
-fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN);
+fun lookup_case_names thm = AList.lookup (op =) (Thm.tags_of_thm thm) cases_tagN;
 
 val save_case_names = put_case_names o lookup_case_names;
 val name = put_case_names o SOME;
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -191,8 +191,8 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-fun mode_tab prtabs mode = if_none (assoc (prtabs, mode)) Symtab.empty;
-fun mode_tabs prtabs modes = List.mapPartial (curry assoc prtabs) (modes @ [""]);
+fun mode_tab prtabs mode = if_none (AList.lookup (op =) prtabs mode) Symtab.empty;
+fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]);
 
 
 (* xprod_to_fmt *)
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/sign.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -327,7 +327,7 @@
   let
     fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
     val tab = List.mapPartial f' (add_names (t, []));
-    fun get x = if_none (assoc_string (tab, x)) x;
+    fun get x = if_none (AList.lookup (op =) tab x) x;
   in get end;
 
 fun typ_mapping f g thy T =
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/sorts.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -180,7 +180,7 @@
 fun mg_domain (classes, arities) a S =
   let
     fun dom c =
-      (case Library.assoc_string (Symtab.lookup_multi (arities, a), c) of
+      (case AList.lookup (op =) (Symtab.lookup_multi (arities, a)) c of
         NONE => raise DOMAIN (a, c)
       | SOME Ss => Ss);
     fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/thm.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -1312,12 +1312,12 @@
         (*unknowns appearing elsewhere be preserved!*)
         val vids = map (#1 o #1 o dest_Var) vars;
         fun rename(t as Var((x,i),T)) =
-                (case assoc_string (al,x) of
+                (case AList.lookup (op =) al x of
                    SOME(y) => if x mem_string vids orelse y mem_string vids then t
                               else Var((y,i),T)
                  | NONE=> t)
           | rename(Abs(x,T,t)) =
-              Abs (if_none (assoc_string (al, x)) x, T, rename t)
+              Abs (if_none (AList.lookup (op =) al x) x, T, rename t)
           | rename(f$t) = rename f $ rename t
           | rename(t) = t;
         fun strip_ren Ai = strip_apply rename (Ai,B)
diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/type.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -150,7 +150,7 @@
 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 =
@@ -223,7 +223,7 @@
     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;
@@ -238,11 +238,11 @@
   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
@@ -464,7 +464,7 @@
   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