--- 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)))
--- 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
--- 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;
--- 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)
--- 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;
--- 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 *)
--- 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);
--- 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;
--- 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 *)
--- 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 =
--- 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);
--- 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)
--- 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