# HG changeset patch # User haftmann # Date 1126188563 -7200 # Node ID 04e21a27c0add7b0cf6b983da07680973b943131 # Parent 7d97f60293ae572cd42c8b1af3967161605f4971 introduces some modern-style AList operations diff -r 7d97f60293ae -r 04e21a27c0ad TFL/tfl.ML --- 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 [] = [] diff -r 7d97f60293ae -r 04e21a27c0ad src/HOL/Tools/primrec_package.ML --- 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; diff -r 7d97f60293ae -r 04e21a27c0ad src/HOL/Tools/refute.ML --- 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 => diff -r 7d97f60293ae -r 04e21a27c0ad src/HOL/ex/SVC_Oracle.ML --- 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*) diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/Isar/context_rules.ML --- 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; diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/Isar/method.ML --- 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; diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/Syntax/parser.ML --- 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*) diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/Syntax/syntax.ML --- 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 diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/proof_general.ML --- 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 diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/proofterm.ML --- 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)); diff -r 7d97f60293ae -r 04e21a27c0ad src/Pure/term.ML --- 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 diff -r 7d97f60293ae -r 04e21a27c0ad src/ZF/Tools/induct_tacs.ML --- 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; diff -r 7d97f60293ae -r 04e21a27c0ad src/ZF/Tools/inductive_package.ML --- 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"; diff -r 7d97f60293ae -r 04e21a27c0ad src/ZF/Tools/primrec_package.ML --- 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),