--- a/src/FOL/simpdata.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/FOL/simpdata.ML Mon Sep 12 18:20:32 2005 +0200
@@ -115,7 +115,7 @@
Const("Trueprop",_) $ p =>
(case head_of p of
Const(a,_) =>
- (case assoc(pairs,a) of
+ (case AList.lookup (op =) pairs a of
SOME(rls) => List.concat (map atoms ([th] RL rls))
| NONE => [th])
| _ => [th])
--- a/src/FOLP/simp.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/FOLP/simp.ML Mon Sep 12 18:20:32 2005 +0200
@@ -179,7 +179,7 @@
fun add_vars (tm,vars) = case tm of
Abs (_,_,body) => add_vars(body,vars)
| r$s => (case head_of tm of
- Const(c,T) => (case assoc(new_asms,c) of
+ Const(c,T) => (case AList.lookup (op =) new_asms c of
NONE => add_vars(r,add_vars(s,vars))
| SOME(al) => add_list(tm,al,vars))
| _ => add_vars(r,add_vars(s,vars)))
--- a/src/FOLP/simpdata.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/FOLP/simpdata.ML Mon Sep 12 18:20:32 2005 +0200
@@ -84,7 +84,7 @@
Const("Trueprop",_) $ p =>
(case head_of p of
Const(a,_) =>
- (case assoc(pairs,a) of
+ (case AList.lookup (op =) pairs a of
SOME(rls) => List.concat (map atoms ([th] RL rls))
| NONE => [th])
| _ => [th])
--- a/src/HOL/Tools/datatype_package.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Mon Sep 12 18:20:32 2005 +0200
@@ -458,7 +458,7 @@
fun count_cases (cs, (_, _, true)) = cs
| count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of
NONE => (body, [cname]) :: cs
- | SOME cnames => overwrite (cs, (body, cnames @ [cname])));
+ | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
val cases' = sort (int_ord o Library.swap o pairself (length o snd))
(Library.foldl count_cases ([], cases));
fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
--- a/src/HOL/Tools/inductive_package.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon Sep 12 18:20:32 2005 +0200
@@ -230,7 +230,7 @@
fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
let val f = prod_factors [] u
- in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end
+ in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
| mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
| mg_prod_factors ts (fs, _) = fs;
--- a/src/HOL/Tools/inductive_realizer.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Sep 12 18:20:32 2005 +0200
@@ -275,7 +275,7 @@
val _ $ (_ $ _ $ S) = concl_of r;
val (Const (s, _), _) = strip_comb S;
val rs = getOpt (assoc (rss, s), []);
- in overwrite (rss, (s, rs @ [r])) end;
+ in AList.update (op =) (s, rs @ [r]) rss end;
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
let
--- a/src/HOL/arith_data.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/arith_data.ML Mon Sep 12 18:20:32 2005 +0200
@@ -241,8 +241,8 @@
fun nT (Type("fun",[N,_])) = N = HOLogic.natT
| nT _ = false;
-fun add_atom(t,m,(p,i)) = (case assoc(p,t) of NONE => ((t,m)::p,i)
- | SOME n => (overwrite(p,(t,ratadd(n,m))), i));
+fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i)
+ | SOME n => (AList.update (op =) (t, ratadd (n, m)) p, i));
exception Zero;
--- a/src/HOL/simpdata.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOL/simpdata.ML Mon Sep 12 18:20:32 2005 +0200
@@ -285,7 +285,7 @@
Const("Trueprop",_) $ p =>
(case head_of p of
Const(a,_) =>
- (case assoc(pairs,a) of
+ (case AList.lookup (op =) pairs a of
SOME(rls) => List.concat (map atoms ([th] RL rls))
| NONE => [th])
| _ => [th])
--- a/src/HOLCF/domain/extender.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOLCF/domain/extender.ML Mon Sep 12 18:20:32 2005 +0200
@@ -65,14 +65,14 @@
| rm_sorts (TVar(s,_)) = TVar(s,[])
and remove_sorts l = map rm_sorts l;
val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
- fun analyse indirect (TFree(v,s)) = (case assoc_string(tvars,v) of
+ fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
| SOME sort => if eq_set_string (s,defaultS) orelse
eq_set_string (s,sort )
then TFree(distinct_name v,sort)
else error ("Inconsistent sort constraint" ^
" for type variable " ^ quote v))
- | analyse indirect (t as Type(s,typl)) = (case assoc_string(dtnvs,s)of
+ | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
NONE => if exists (fn x => x = s) indirect_ok
then Type(s,map (analyse false) typl)
else Type(s,map (analyse true) typl)
--- a/src/HOLCF/domain/library.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOLCF/domain/library.ML Mon Sep 12 18:20:32 2005 +0200
@@ -63,7 +63,7 @@
fun mk_var_names ids : string list = let
fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
fun index_vnames(vn::vns,occupied) =
- (case assoc(occupied,vn) of
+ (case AList.lookup (op =) occupied vn of
NONE => if vn mem vns
then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied)
else vn :: index_vnames(vns, occupied)
--- a/src/HOLCF/pcpodef_package.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOLCF/pcpodef_package.ML Mon Sep 12 18:20:32 2005 +0200
@@ -79,7 +79,7 @@
else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
(*lhs*)
- val lhs_tfrees = map (fn v => (v, getOpt (assoc (rhs_tfrees, v), HOLogic.typeS))) vs;
+ val lhs_tfrees = map (fn v => (v, AList.lookup (op =) rhs_tfrees v |> the_default HOLogic.typeS)) vs;
val lhs_sorts = map snd lhs_tfrees;
val tname = Syntax.type_name t mx;
val full_tname = full tname;
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Sep 12 18:20:32 2005 +0200
@@ -492,7 +492,7 @@
end;
fun coeff poly atom : IntInf.int =
- case assoc(poly,atom) of NONE => 0 | SOME i => i;
+ AList.lookup (op =) poly atom |> the_default 0;
fun lcms is = Library.foldl lcm (1, is);
--- a/src/Provers/splitter.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/Provers/splitter.ML Mon Sep 12 18:20:32 2005 +0200
@@ -332,7 +332,7 @@
(case strip_comb lhs of (Const(a,aT),args) =>
let val info = (aT,lhs,thm,fastype_of t,length args)
in case AList.lookup (op =) cmap a of
- SOME infos => overwrite(cmap,(a,info::infos))
+ SOME infos => AList.update (op =) (a, info::infos) cmap
| NONE => (a,[info])::cmap
end
| _ => split_format_err())
--- a/src/Pure/drule.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/Pure/drule.ML Mon Sep 12 18:20:32 2005 +0200
@@ -302,8 +302,8 @@
val frees = map dest_Free (term_frees big);
val tvars = term_tvars big;
val tfrees = term_tfrees big;
- fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i));
- fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
+ fun typ(a,i) = if i<0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a,i);
+ fun sort(a,i) = if i<0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a,i);
in (typ,sort) end;
fun add_used thm used =
@@ -344,7 +344,7 @@
val internalK = "internal";
fun get_kind thm =
- (case Library.assoc (#2 (Thm.get_name_tags thm), "kind") of
+ (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of
SOME (k :: _) => k
| _ => "unknown");
@@ -479,7 +479,7 @@
val alist = foldr newName [] vars
fun mk_inst (Var(v,T)) =
(cterm_of thy (Var(v,T)),
- cterm_of thy (Free(valOf (assoc(alist,v)), T)))
+ cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
val insts = map mk_inst vars
fun thaw i th' = (*i is non-negative increment for Var indexes*)
th' |> forall_intr_list (map #2 insts)
@@ -503,7 +503,7 @@
(prop :: Thm.terms_of_tpairs tpairs, [])) vars
fun mk_inst (Var(v,T)) =
(cterm_of thy (Var(v,T)),
- cterm_of thy (Free(valOf (assoc(alist,v)), T)))
+ cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
val insts = map mk_inst vars
fun thaw th' =
th' |> forall_intr_list (map #2 insts)
@@ -999,7 +999,7 @@
| rename_bvars vs thm =
let
val {thy, prop, ...} = rep_thm thm;
- fun ren (Abs (x, T, t)) = Abs (getOpt (assoc (vs, x), x), T, ren t)
+ fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
| ren (t $ u) = ren t $ ren u
| ren t = t;
in equal_elim (reflexive (cterm_of thy (ren prop))) thm end;
--- a/src/Pure/goals.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/Pure/goals.ML Mon Sep 12 18:20:32 2005 +0200
@@ -310,7 +310,7 @@
(* get theorems *)
-fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
+fun get_thm_locale name ((_, {thms, ...}: locale)) = AList.lookup (op =) thms name;
fun get_thmx f get thy name =
(case get_first (get_thm_locale name) (get_scope thy) of
@@ -338,7 +338,7 @@
fun read_typ thy (envT, s) =
let
- fun def_sort (x, ~1) = assoc (envT, x)
+ fun def_sort (x, ~1) = AList.lookup (op =) envT x
| def_sort _ = NONE;
val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg;
in (Term.add_typ_tfrees (T, envT), T) end;
@@ -357,9 +357,9 @@
fun read_axm thy ((envS, envT, used), (name, s)) =
let
- fun def_sort (x, ~1) = assoc (envS, x)
+ fun def_sort (x, ~1) = AList.lookup (op =) envS x
| def_sort _ = NONE;
- fun def_type (x, ~1) = assoc (envT, x)
+ fun def_type (x, ~1) = AList.lookup (op =) envT x
| def_type _ = NONE;
val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s);
in
@@ -382,9 +382,9 @@
val envS = List.concat (map #1 defaults);
val envT = List.concat (map #2 defaults);
val used = List.concat (map #3 defaults);
- fun def_sort (x, ~1) = assoc (envS, x)
+ fun def_sort (x, ~1) = AList.lookup (op =) envS x
| def_sort _ = NONE;
- fun def_type (x, ~1) = assoc (envT, x)
+ fun def_type (x, ~1) = AList.lookup (op =) envT x
| def_type _ = NONE;
in (if (is_open_loc thy)
then (#1 o read_def_cterm (thy, def_type, def_sort) used true)
--- a/src/Pure/proofterm.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/Pure/proofterm.ML Mon Sep 12 18:20:32 2005 +0200
@@ -470,10 +470,10 @@
(**** Freezing and thawing of variables in proof terms ****)
fun frzT names =
- map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs));
+ map_type_tvar (fn (ixn, xs) => TFree ((the o AList.lookup (op =) names) ixn, xs));
fun thawT names =
- map_type_tfree (fn (s, xs) => case assoc (names, s) of
+ map_type_tfree (fn (s, xs) => case AList.lookup (op =) names s of
NONE => TFree (s, xs)
| SOME ixn => TVar (ixn, xs));
@@ -484,7 +484,7 @@
| freeze names names' (Const (s, T)) = Const (s, frzT names' T)
| freeze names names' (Free (s, T)) = Free (s, frzT names' T)
| freeze names names' (Var (ixn, T)) =
- Free (the (assoc (names, ixn)), frzT names' T)
+ Free ((the o AList.lookup (op =) names) ixn, frzT names' T)
| freeze names names' t = t;
fun thaw names names' (t $ u) =
@@ -494,7 +494,7 @@
| thaw names names' (Const (s, T)) = Const (s, thawT names' T)
| thaw names names' (Free (s, T)) =
let val T' = thawT names' T
- in case assoc (names, s) of
+ in case AList.lookup (op =) names s of
NONE => Free (s, T')
| SOME ixn => Var (ixn, T')
end
@@ -566,7 +566,7 @@
let val v = variant used (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
-fun freeze_one alist (ix, sort) = (case assoc (alist, ix) of
+fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
NONE => TVar (ix, sort)
| SOME name => TFree (name, sort));
@@ -892,7 +892,7 @@
val (ts', ts'') = splitAt (length vs, ts)
val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
- ixn ins (case assoc (insts, ixn) of
+ ixn ins (case AList.lookup (op =) insts ixn of
SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
| _ => ixns union ixns'))
(needed prop ts'' prfs, add_npvars false true [] ([], prop));
@@ -982,7 +982,7 @@
let
val substT = Envir.typ_subst_TVars tyinsts;
- fun subst' lev (t as Var (ixn, _)) = (case assoc (insts, ixn) of
+ fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
NONE => t
| SOME u => incr_boundvars lev u)
| subst' lev (Const (s, T)) = Const (s, substT T)
@@ -997,7 +997,7 @@
Abst (a, Option.map substT T, subst plev (tlev+1) body)
| subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf'
| subst plev tlev (prf % t) = subst plev tlev prf % Option.map (subst' tlev) t
- | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case assoc (pinst, ixn) of
+ | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case AList.lookup (op =) pinst ixn of
NONE => prf
| SOME prf' => incr_pboundvars plev tlev prf')
| subst _ _ (PThm (id, prf, prop, Ts)) =
--- a/src/ZF/simpdata.ML Mon Sep 12 17:29:07 2005 +0200
+++ b/src/ZF/simpdata.ML Mon Sep 12 18:20:32 2005 +0200
@@ -15,7 +15,7 @@
let fun tryrules pairs t =
case head_of t of
Const(a,_) =>
- (case assoc(pairs,a) of
+ (case AList.lookup (op =) pairs a of
SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
([th] RL rls))
| NONE => [th])