--- a/TFL/tfl.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/TFL/tfl.ML Thu Sep 08 16:09:23 2005 +0200
@@ -621,7 +621,7 @@
let val (qvars,body) = S.strip_exists tm
val vlist = #2(S.strip_comb (S.rhs body))
val plist = ListPair.zip (vlist, xlist)
- val args = map (fn qv => valOf (gen_assoc (op aconv) (plist, qv))) qvars
+ val args = map (the o AList.lookup (op aconv) plist) qvars
handle Option => sys_error
"TFL fault [alpha_ex_unroll]: no correspondence"
fun build ex [] = []
--- a/src/HOL/Tools/primrec_package.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Sep 08 16:09:23 2005 +0200
@@ -81,10 +81,8 @@
else if rpos <> rpos' then
raise RecError "position of recursive argument inconsistent"
else
- overwrite (rec_fns,
- (fnameT,
- (tname, rpos,
- (cname, (ls, cargs, rs, rhs, eq))::eqns))))
+ AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
+ rec_fns)
end
handle RecError s => primrec_eq_err sign s eq;
--- a/src/HOL/Tools/refute.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/HOL/Tools/refute.ML Thu Sep 08 16:09:23 2005 +0200
@@ -271,7 +271,7 @@
let
val {interpreters, printers, parameters} = RefuteData.get thy
in
- case assoc (interpreters, name) of
+ case AList.lookup (op =) interpreters name of
NONE => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
| SOME _ => error ("Interpreter " ^ name ^ " already declared")
end;
@@ -282,7 +282,7 @@
let
val {interpreters, printers, parameters} = RefuteData.get thy
in
- case assoc (printers, name) of
+ case AList.lookup (op =) printers name of
NONE => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
| SOME _ => error ("Printer " ^ name ^ " already declared")
end;
@@ -335,14 +335,14 @@
let
(* (string * string) list * string -> int *)
fun read_int (parms, name) =
- case assoc_string (parms, name) of
+ case AList.lookup (op =) parms name of
SOME s => (case Int.fromString s of
SOME i => i
| NONE => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
| NONE => error ("parameter " ^ quote name ^ " must be assigned a value")
(* (string * string) list * string -> string *)
fun read_string (parms, name) =
- case assoc_string (parms, name) of
+ case AList.lookup (op =) parms name of
SOME s => s
| NONE => error ("parameter " ^ quote name ^ " must be assigned a value")
(* (string * string) list *)
@@ -382,12 +382,12 @@
fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
(* replace a 'DtTFree' variable by the associated type *)
- (valOf o assoc) (typ_assoc, DatatypeAux.DtTFree a)
+ (the o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a)
| typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
Type (s, map (typ_of_dtyp descr typ_assoc) ds)
| typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
let
- val (s, ds, _) = (valOf o assoc) (descr, i)
+ val (s, ds, _) = (the o AList.lookup (op =) descr) i
in
Type (s, map (typ_of_dtyp descr typ_assoc) ds)
end;
@@ -590,7 +590,7 @@
| Const ("arbitrary", T) => collect_type_axioms (axs, T)
| Const ("The", T) =>
let
- val ax = specialize_type (("The", T), (valOf o assoc) (axioms, "HOL.the_eq_trivial"))
+ val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
in
if mem_term (ax, axs) then
collect_type_axioms (axs, T)
@@ -600,7 +600,8 @@
end
| Const ("Hilbert_Choice.Eps", T) =>
let
- val ax = specialize_type (("Hilbert_Choice.Eps", T), (valOf o assoc) (axioms, "Hilbert_Choice.someI"))
+ val ax = specialize_type (("Hilbert_Choice.Eps", T),
+ (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
in
if mem_term (ax, axs) then
collect_type_axioms (axs, T)
@@ -690,7 +691,8 @@
val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
(* Term.term option *)
val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
- val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
+ val intro_ax = (Option.map (fn t => specialize_type ((s, T), t))
+ (AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
val axs' = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
(* collect relevant type axioms *)
collect_type_axioms (axs, T)
@@ -776,7 +778,7 @@
let
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
+ val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
val typ_assoc = dtyps ~~ Ts
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = (if Library.exists (fn d =>
@@ -829,7 +831,7 @@
fun first_universe xs sizes minsize =
let
fun size_of_typ T =
- case assoc (sizes, string_of_typ T) of
+ case AList.lookup (op =) sizes (string_of_typ T) of
SOME n => n
| NONE => minsize
in
@@ -876,7 +878,7 @@
(* continue search *)
next max (len+1) (sum+x1) (x2::xs)
(* only consider those types for which the size is not fixed *)
- val mutables = List.filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
+ val mutables = List.filter (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
(* subtract 'minsize' from every size (will be added again at the end) *)
val diffs = map (fn (_, n) => n-minsize) mutables
in
@@ -884,7 +886,7 @@
SOME diffs' =>
(* merge with those types for which the size is fixed *)
SOME (snd (foldl_map (fn (ds, (T, _)) =>
- case assoc (sizes, string_of_typ T) of
+ case AList.lookup (op =) sizes (string_of_typ T) of
SOME n => (ds, (T, n)) (* return the fixed size *)
| NONE => (tl ds, (T, minsize + hd ds))) (* consume the head of 'ds', add 'minsize' *)
(diffs', xs)))
@@ -949,7 +951,7 @@
let
val index = #index info
val descr = #descr info
- val (_, _, constrs) = (valOf o assoc) (descr, index)
+ val (_, _, constrs) = (the o AList.lookup (op =) descr) index
in
(* recursive datatype? *)
Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs
@@ -1358,7 +1360,7 @@
(* unit -> (interpretation * model * arguments) option *)
fun interpret_groundtype () =
let
- val size = (if T = Term.propT then 2 else (valOf o assoc) (typs, T)) (* the model MUST specify a size for ground types *)
+ val size = (if T = Term.propT then 2 else (the o AList.lookup (op =) typs) T) (* the model MUST specify a size for ground types *)
val next = next_idx+size
val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
(* prop_formula list *)
@@ -1407,7 +1409,7 @@
| TVar _ => interpret_groundtype ()
end
in
- case assoc (terms, t) of
+ case AList.lookup (op =) terms t of
SOME intr =>
(* return an existing interpretation *)
SOME (intr, model, args)
@@ -1598,7 +1600,7 @@
let
val (typs, terms) = model
in
- case assoc (terms, t) of
+ case AList.lookup (op =) terms t of
SOME intr =>
(* return an existing interpretation *)
SOME (intr, model, args)
@@ -1651,7 +1653,7 @@
SOME info => (* inductive datatype *)
let
(* int option -- only recursive IDTs have an associated depth *)
- val depth = assoc (typs, Type (s, Ts))
+ val depth = AList.lookup (op =) typs (Type (s, Ts))
in
if depth = (SOME 0) then (* termination condition to avoid infinite recursion *)
(* return a leaf of size 0 *)
@@ -1660,7 +1662,7 @@
let
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
+ val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
val typ_assoc = dtyps ~~ Ts
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = (if Library.exists (fn d =>
@@ -1670,7 +1672,8 @@
else
())
(* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
- val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s, Ts), n-1)))
+ val typs' = case depth of NONE => typs | SOME n =>
+ AList.update (op =) (Type (s, Ts), n-1) typs
(* recursively compute the size of the datatype *)
val size = size_of_dtyp thy typs' descr typ_assoc constrs
val next_idx = #next_idx args
@@ -1695,7 +1698,7 @@
| interpret_term _ = (* a (free or schematic) type variable *)
NONE
in
- case assoc (terms, t) of
+ case AList.lookup (op =) terms t of
SOME intr =>
(* return an existing interpretation *)
SOME (intr, model, args)
@@ -1713,7 +1716,7 @@
let
val (typs, terms) = model
in
- case assoc (terms, t) of
+ case AList.lookup (op =) terms t of
SOME intr =>
(* return an existing interpretation *)
SOME (intr, model, args)
@@ -1727,7 +1730,7 @@
let
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
+ val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
val typ_assoc = dtyps ~~ Ts'
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = (if Library.exists (fn d =>
@@ -1751,8 +1754,9 @@
val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type (s', Ts')))
val total = size_of_type i
(* int option -- only recursive IDTs have an associated depth *)
- val depth = assoc (typs, Type (s', Ts'))
- val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
+ val depth = AList.lookup (op =) typs (Type (s', Ts'))
+ val typs' = (case depth of NONE => typs | SOME n =>
+ AList.update (op =) (Type (s', Ts'), n-1) typs)
(* returns an interpretation where everything is mapped to "undefined" *)
(* DatatypeAux.dtyp list -> interpretation *)
fun make_undef [] =
@@ -1904,7 +1908,7 @@
let
val index = #index info
val descr = #descr info
- val (dtname, dtyps, _) = (valOf o assoc) (descr, index)
+ val (dtname, dtyps, _) = (the o AList.lookup (op =) descr) index
(* number of all constructors, including those of different *)
(* (mutually recursive) datatypes within the same descriptor 'descr' *)
val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs) descr)
@@ -1995,7 +1999,7 @@
SOME args => (n, args)
| NONE => get_cargs_rec (n+1, xs))
in
- get_cargs_rec (0, (valOf o assoc) (mc_intrs, idx))
+ get_cargs_rec (0, (the o AList.lookup (op =) mc_intrs) idx)
end
(* returns the number of constructors in datatypes that occur in *)
(* the descriptor 'descr' before the datatype given by 'idx' *)
@@ -2015,7 +2019,7 @@
(* where 'idx' gives the datatype and 'elem' the element of it *)
(* int -> int -> interpretation *)
fun compute_array_entry idx elem =
- case Array.sub ((valOf o assoc) (INTRS, idx), elem) of
+ case Array.sub ((the o AList.lookup (op =) INTRS) idx, elem) of
SOME result =>
(* simply return the previously computed result *)
result
@@ -2033,7 +2037,7 @@
(* select the correct subtree of the parameter corresponding to constructor 'c' *)
val p_intr = select_subtree (List.nth (p_intrs, get_coffset idx + c), args)
(* find the indices of the constructor's recursive arguments *)
- val (_, _, constrs) = (valOf o assoc) (descr, idx)
+ val (_, _, constrs) = (the o AList.lookup (op =) descr) idx
val constr_args = (snd o List.nth) (constrs, c)
val rec_args = List.filter (DatatypeAux.is_rec_type o fst) (constr_args ~~ args)
val rec_args' = map (fn (dtyp, elem) => (DatatypeAux.dest_DtRec dtyp, elem)) rec_args
@@ -2041,7 +2045,7 @@
val result = foldl (fn ((idx, elem), intr) =>
interpretation_apply (intr, compute_array_entry idx elem)) p_intr rec_args'
(* update 'INTRS' *)
- val _ = Array.update ((valOf o assoc) (INTRS, idx), elem, SOME result)
+ val _ = Array.update ((the o AList.lookup (op =) INTRS) idx, elem, SOME result)
in
result
end
@@ -2060,13 +2064,13 @@
in
modifyi_loop 0
end
- val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index))
+ val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((the o AList.lookup (op =) INTRS) index)
(* 'a Array.array -> 'a list *)
fun toList arr =
Array.foldr op:: [] arr
in
(* return the part of 'INTRS' that corresponds to the current datatype *)
- SOME ((Node o (map valOf) o toList o valOf o assoc) (INTRS, index), model', args')
+ SOME ((Node o map the o toList o the o AList.lookup (op =) INTRS) index, model', args')
end
end
else
@@ -2515,7 +2519,7 @@
val (typs, _) = model
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
+ val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
val typ_assoc = dtyps ~~ Ts
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = (if Library.exists (fn d =>
--- a/src/HOL/ex/SVC_Oracle.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/HOL/ex/SVC_Oracle.ML Thu Sep 08 16:09:23 2005 +0200
@@ -38,7 +38,7 @@
case t of
Free _ => t (*but not existing Vars, lest the names clash*)
| Bound _ => t
- | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
+ | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
SOME v => v
| NONE => insert t)
(*abstraction of a numeric literal*)
--- a/src/Pure/Isar/context_rules.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML Thu Sep 08 16:09:23 2005 +0200
@@ -111,7 +111,7 @@
fun print_rules prt x (Rules {rules, ...}) =
let
fun prt_kind (i, b) =
- Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
+ Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
(List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
(sort (int_ord o pairself fst) rules));
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
--- a/src/Pure/Isar/method.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/Isar/method.ML Thu Sep 08 16:09:23 2005 +0200
@@ -383,7 +383,7 @@
val params = rev(Term.rename_wrt_term Bi params)
(* as they are printed: bound variables with *)
(* the same name are renamed during printing *)
- fun types' (a, ~1) = (case assoc (params, a) of
+ fun types' (a, ~1) = (case AList.lookup (op =) params a of
NONE => types (a, ~1)
| some => some)
| types' xi = types xi;
--- a/src/Pure/Syntax/parser.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Sep 08 16:09:23 2005 +0200
@@ -724,7 +724,7 @@
(_, _, _, Nonterminal (nt, minPrec) :: _, _, _) =>
let (*predictor operation*)
val (used', new_states) =
- (case assoc (used, nt) of
+ (case AList.lookup (op =) used nt of
SOME (usedPrec, l) => (*nonterminal has been processed*)
if usedPrec <= minPrec then
(*wanted precedence has been processed*)
--- a/src/Pure/Syntax/syntax.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Sep 08 16:09:23 2005 +0200
@@ -110,7 +110,7 @@
fun lookup_tokentr tabs modes =
let val trs = gen_distinct eq_fst
(List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
- in fn c => Option.map fst (assoc (trs, c)) end;
+ in fn c => Option.map fst (AList.lookup (op =) trs c) end;
fun merge_tokentrtabs tabs1 tabs2 =
let
--- a/src/Pure/proof_general.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/proof_general.ML Thu Sep 08 16:09:23 2005 +0200
@@ -1116,12 +1116,12 @@
fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
fun setpref name value =
- (case assoc (allprefs(), name) of
+ (case AList.lookup (op =) (allprefs ()) name of
NONE => warning ("Unknown pref: " ^ quote name)
| SOME (_, (_, _, set)) => set value);
fun getpref name =
- (case assoc (allprefs(), name) of
+ (case AList.lookup (op =) (allprefs ()) name of
NONE => warning ("Unknown pref: " ^ quote name)
| SOME (_, (_, (_,get), _)) =>
issue_pgip "prefval" [("name", name)] (get ()));
@@ -1164,7 +1164,7 @@
(* Proof control commands *)
local
- fun xmlattro attr attrs = assoc(attrs,attr)
+ fun xmlattro attr attrs = AList.lookup (op =) attrs attr
fun xmlattr attr attrs =
(case xmlattro attr attrs of
--- a/src/Pure/proofterm.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/proofterm.ML Thu Sep 08 16:09:23 2005 +0200
@@ -470,7 +470,7 @@
(**** Freezing and thawing of variables in proof terms ****)
fun frzT names =
- map_type_tvar (fn (ixn, xs) => TFree (valOf (assoc (names, ixn)), xs));
+ map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs));
fun thawT names =
map_type_tfree (fn (s, xs) => case assoc (names, s) of
@@ -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 (valOf (assoc (names, ixn)), frzT names' T)
+ Free (the (assoc (names, ixn)), frzT names' T)
| freeze names names' t = t;
fun thaw names names' (t $ u) =
@@ -553,7 +553,7 @@
val ixns = add_term_tvar_ixns (t, []);
val fmap = fs ~~ 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 b => TVar ((b, 0), S));
in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
@@ -810,8 +810,9 @@
| add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
and add_npvars' Ts (vs, t) = (case strip_comb t of
(Var (ixn, _), ts) => if test_args [] ts then vs
- else Library.foldl (add_npvars' Ts) (overwrite (vs,
- (ixn, Library.foldl (add_funvars Ts) (getOpt (assoc (vs, ixn), []), ts))), ts)
+ else Library.foldl (add_npvars' Ts)
+ (AList.update (op =) (ixn,
+ Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts)
| (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
| (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
--- a/src/Pure/term.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/Pure/term.ML Thu Sep 08 16:09:23 2005 +0200
@@ -861,7 +861,7 @@
fun subst_free [] = (fn t=>t)
| subst_free pairs =
let fun substf u =
- case gen_assoc (op aconv) (pairs, u) of
+ case AList.lookup (op aconv) pairs u of
SOME u' => u'
| NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
| t$u' => substf t $ substf u'
@@ -916,7 +916,7 @@
let
fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
| subst (t $ u) = subst t $ subst u
- | subst t = if_none (gen_assoc (op aconv) (inst, t)) t;
+ | subst t = if_none (AList.lookup (op aconv) inst t) t;
in subst tm end;
(*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*)
@@ -924,7 +924,7 @@
| typ_subst_atomic inst ty =
let
fun subst (Type (a, Ts)) = Type (a, map subst Ts)
- | subst T = if_none (gen_assoc (op = : typ * typ -> bool) (inst, T)) T;
+ | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
in subst ty end;
fun subst_atomic_types [] tm = tm
@@ -977,7 +977,7 @@
let
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
| subst_typ (TVar v) =
- (case gen_assoc eq_tvar (instT, v) of
+ (case AList.lookup eq_tvar instT v of
SOME T => T
| NONE => raise SAME)
| subst_typ _ = raise SAME
@@ -995,7 +995,7 @@
| subst (Free (x, T)) = Free (x, substT T)
| subst (Var (xi, T)) =
let val (T', same) = (substT T, false) handle SAME => (T, true) in
- (case gen_assoc eq_var (inst, (xi, T')) of
+ (case AList.lookup eq_var inst (xi, T') of
SOME t => t
| NONE => if same then raise SAME else Var (xi, T'))
end
--- a/src/ZF/Tools/induct_tacs.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Thu Sep 08 16:09:23 2005 +0200
@@ -84,7 +84,7 @@
| mk_pair _ = raise Match
val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
(#2 (strip_context Bi))
- in case assoc (pairs, var) of
+ in case AList.lookup (op =) pairs var of
NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
| SOME t => t
end;
--- a/src/ZF/Tools/inductive_package.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Sep 08 16:09:23 2005 +0200
@@ -300,7 +300,7 @@
prem is a premise of an intr rule*)
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
(Const("op :",_)$t$X), iprems) =
- (case gen_assoc (op aconv) (ind_alist, X) of
+ (case AList.lookup (op aconv) ind_alist X of
SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
let fun mk_sb (rec_tm,pred) =
@@ -314,7 +314,7 @@
val iprems = foldr (add_induct_prem ind_alist) []
(Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr
- val (SOME pred) = gen_assoc (op aconv) (ind_alist, X)
+ val (SOME pred) = AList.lookup (op aconv) ind_alist X
val concl = FOLogic.mk_Trueprop (pred $ t)
in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
handle Bind => error"Recursion term not found in conclusion";
--- a/src/ZF/Tools/primrec_package.ML Thu Sep 08 16:08:50 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML Thu Sep 08 16:09:23 2005 +0200
@@ -80,7 +80,7 @@
else case rec_fn_opt of
NONE => SOME (fname, ftype, ls, rs, con_info, [new_eqn])
| SOME (fname', _, ls', rs', con_info': constructor_info, eqns) =>
- if isSome (assoc (eqns, cname)) then
+ if AList.defined (op =) eqns cname then
raise RecError "constructor already occurred as pattern"
else if (ls <> ls') orelse (rs <> rs') then
raise RecError "non-recursive arguments are inconsistent"
@@ -120,7 +120,7 @@
Missing cases are replaced by 0 and all cases are put into order.*)
fun add_case ((cname, recursor_pair), cases) =
let val (rhs, recursor_rhs, eq) =
- case assoc (eqns, cname) of
+ case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
(Const ("0", Ind_Syntax.iT),