1.1 --- a/TFL/tfl.ML Thu Sep 08 16:08:50 2005 +0200
1.2 +++ b/TFL/tfl.ML Thu Sep 08 16:09:23 2005 +0200
1.3 @@ -621,7 +621,7 @@
1.4 let val (qvars,body) = S.strip_exists tm
1.5 val vlist = #2(S.strip_comb (S.rhs body))
1.6 val plist = ListPair.zip (vlist, xlist)
1.7 - val args = map (fn qv => valOf (gen_assoc (op aconv) (plist, qv))) qvars
1.8 + val args = map (the o AList.lookup (op aconv) plist) qvars
1.9 handle Option => sys_error
1.10 "TFL fault [alpha_ex_unroll]: no correspondence"
1.11 fun build ex [] = []
2.1 --- a/src/HOL/Tools/primrec_package.ML Thu Sep 08 16:08:50 2005 +0200
2.2 +++ b/src/HOL/Tools/primrec_package.ML Thu Sep 08 16:09:23 2005 +0200
2.3 @@ -81,10 +81,8 @@
2.4 else if rpos <> rpos' then
2.5 raise RecError "position of recursive argument inconsistent"
2.6 else
2.7 - overwrite (rec_fns,
2.8 - (fnameT,
2.9 - (tname, rpos,
2.10 - (cname, (ls, cargs, rs, rhs, eq))::eqns))))
2.11 + AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
2.12 + rec_fns)
2.13 end
2.14 handle RecError s => primrec_eq_err sign s eq;
2.15
3.1 --- a/src/HOL/Tools/refute.ML Thu Sep 08 16:08:50 2005 +0200
3.2 +++ b/src/HOL/Tools/refute.ML Thu Sep 08 16:09:23 2005 +0200
3.3 @@ -271,7 +271,7 @@
3.4 let
3.5 val {interpreters, printers, parameters} = RefuteData.get thy
3.6 in
3.7 - case assoc (interpreters, name) of
3.8 + case AList.lookup (op =) interpreters name of
3.9 NONE => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
3.10 | SOME _ => error ("Interpreter " ^ name ^ " already declared")
3.11 end;
3.12 @@ -282,7 +282,7 @@
3.13 let
3.14 val {interpreters, printers, parameters} = RefuteData.get thy
3.15 in
3.16 - case assoc (printers, name) of
3.17 + case AList.lookup (op =) printers name of
3.18 NONE => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
3.19 | SOME _ => error ("Printer " ^ name ^ " already declared")
3.20 end;
3.21 @@ -335,14 +335,14 @@
3.22 let
3.23 (* (string * string) list * string -> int *)
3.24 fun read_int (parms, name) =
3.25 - case assoc_string (parms, name) of
3.26 + case AList.lookup (op =) parms name of
3.27 SOME s => (case Int.fromString s of
3.28 SOME i => i
3.29 | NONE => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
3.30 | NONE => error ("parameter " ^ quote name ^ " must be assigned a value")
3.31 (* (string * string) list * string -> string *)
3.32 fun read_string (parms, name) =
3.33 - case assoc_string (parms, name) of
3.34 + case AList.lookup (op =) parms name of
3.35 SOME s => s
3.36 | NONE => error ("parameter " ^ quote name ^ " must be assigned a value")
3.37 (* (string * string) list *)
3.38 @@ -382,12 +382,12 @@
3.39
3.40 fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
3.41 (* replace a 'DtTFree' variable by the associated type *)
3.42 - (valOf o assoc) (typ_assoc, DatatypeAux.DtTFree a)
3.43 + (the o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a)
3.44 | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
3.45 Type (s, map (typ_of_dtyp descr typ_assoc) ds)
3.46 | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
3.47 let
3.48 - val (s, ds, _) = (valOf o assoc) (descr, i)
3.49 + val (s, ds, _) = (the o AList.lookup (op =) descr) i
3.50 in
3.51 Type (s, map (typ_of_dtyp descr typ_assoc) ds)
3.52 end;
3.53 @@ -590,7 +590,7 @@
3.54 | Const ("arbitrary", T) => collect_type_axioms (axs, T)
3.55 | Const ("The", T) =>
3.56 let
3.57 - val ax = specialize_type (("The", T), (valOf o assoc) (axioms, "HOL.the_eq_trivial"))
3.58 + val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
3.59 in
3.60 if mem_term (ax, axs) then
3.61 collect_type_axioms (axs, T)
3.62 @@ -600,7 +600,8 @@
3.63 end
3.64 | Const ("Hilbert_Choice.Eps", T) =>
3.65 let
3.66 - val ax = specialize_type (("Hilbert_Choice.Eps", T), (valOf o assoc) (axioms, "Hilbert_Choice.someI"))
3.67 + val ax = specialize_type (("Hilbert_Choice.Eps", T),
3.68 + (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
3.69 in
3.70 if mem_term (ax, axs) then
3.71 collect_type_axioms (axs, T)
3.72 @@ -690,7 +691,8 @@
3.73 val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
3.74 (* Term.term option *)
3.75 val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
3.76 - val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
3.77 + val intro_ax = (Option.map (fn t => specialize_type ((s, T), t))
3.78 + (AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
3.79 val axs' = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
3.80 (* collect relevant type axioms *)
3.81 collect_type_axioms (axs, T)
3.82 @@ -776,7 +778,7 @@
3.83 let
3.84 val index = #index info
3.85 val descr = #descr info
3.86 - val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
3.87 + val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
3.88 val typ_assoc = dtyps ~~ Ts
3.89 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
3.90 val _ = (if Library.exists (fn d =>
3.91 @@ -829,7 +831,7 @@
3.92 fun first_universe xs sizes minsize =
3.93 let
3.94 fun size_of_typ T =
3.95 - case assoc (sizes, string_of_typ T) of
3.96 + case AList.lookup (op =) sizes (string_of_typ T) of
3.97 SOME n => n
3.98 | NONE => minsize
3.99 in
3.100 @@ -876,7 +878,7 @@
3.101 (* continue search *)
3.102 next max (len+1) (sum+x1) (x2::xs)
3.103 (* only consider those types for which the size is not fixed *)
3.104 - val mutables = List.filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
3.105 + val mutables = List.filter (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
3.106 (* subtract 'minsize' from every size (will be added again at the end) *)
3.107 val diffs = map (fn (_, n) => n-minsize) mutables
3.108 in
3.109 @@ -884,7 +886,7 @@
3.110 SOME diffs' =>
3.111 (* merge with those types for which the size is fixed *)
3.112 SOME (snd (foldl_map (fn (ds, (T, _)) =>
3.113 - case assoc (sizes, string_of_typ T) of
3.114 + case AList.lookup (op =) sizes (string_of_typ T) of
3.115 SOME n => (ds, (T, n)) (* return the fixed size *)
3.116 | NONE => (tl ds, (T, minsize + hd ds))) (* consume the head of 'ds', add 'minsize' *)
3.117 (diffs', xs)))
3.118 @@ -949,7 +951,7 @@
3.119 let
3.120 val index = #index info
3.121 val descr = #descr info
3.122 - val (_, _, constrs) = (valOf o assoc) (descr, index)
3.123 + val (_, _, constrs) = (the o AList.lookup (op =) descr) index
3.124 in
3.125 (* recursive datatype? *)
3.126 Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs
3.127 @@ -1358,7 +1360,7 @@
3.128 (* unit -> (interpretation * model * arguments) option *)
3.129 fun interpret_groundtype () =
3.130 let
3.131 - val size = (if T = Term.propT then 2 else (valOf o assoc) (typs, T)) (* the model MUST specify a size for ground types *)
3.132 + 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 *)
3.133 val next = next_idx+size
3.134 val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
3.135 (* prop_formula list *)
3.136 @@ -1407,7 +1409,7 @@
3.137 | TVar _ => interpret_groundtype ()
3.138 end
3.139 in
3.140 - case assoc (terms, t) of
3.141 + case AList.lookup (op =) terms t of
3.142 SOME intr =>
3.143 (* return an existing interpretation *)
3.144 SOME (intr, model, args)
3.145 @@ -1598,7 +1600,7 @@
3.146 let
3.147 val (typs, terms) = model
3.148 in
3.149 - case assoc (terms, t) of
3.150 + case AList.lookup (op =) terms t of
3.151 SOME intr =>
3.152 (* return an existing interpretation *)
3.153 SOME (intr, model, args)
3.154 @@ -1651,7 +1653,7 @@
3.155 SOME info => (* inductive datatype *)
3.156 let
3.157 (* int option -- only recursive IDTs have an associated depth *)
3.158 - val depth = assoc (typs, Type (s, Ts))
3.159 + val depth = AList.lookup (op =) typs (Type (s, Ts))
3.160 in
3.161 if depth = (SOME 0) then (* termination condition to avoid infinite recursion *)
3.162 (* return a leaf of size 0 *)
3.163 @@ -1660,7 +1662,7 @@
3.164 let
3.165 val index = #index info
3.166 val descr = #descr info
3.167 - val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
3.168 + val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
3.169 val typ_assoc = dtyps ~~ Ts
3.170 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
3.171 val _ = (if Library.exists (fn d =>
3.172 @@ -1670,7 +1672,8 @@
3.173 else
3.174 ())
3.175 (* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
3.176 - val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s, Ts), n-1)))
3.177 + val typs' = case depth of NONE => typs | SOME n =>
3.178 + AList.update (op =) (Type (s, Ts), n-1) typs
3.179 (* recursively compute the size of the datatype *)
3.180 val size = size_of_dtyp thy typs' descr typ_assoc constrs
3.181 val next_idx = #next_idx args
3.182 @@ -1695,7 +1698,7 @@
3.183 | interpret_term _ = (* a (free or schematic) type variable *)
3.184 NONE
3.185 in
3.186 - case assoc (terms, t) of
3.187 + case AList.lookup (op =) terms t of
3.188 SOME intr =>
3.189 (* return an existing interpretation *)
3.190 SOME (intr, model, args)
3.191 @@ -1713,7 +1716,7 @@
3.192 let
3.193 val (typs, terms) = model
3.194 in
3.195 - case assoc (terms, t) of
3.196 + case AList.lookup (op =) terms t of
3.197 SOME intr =>
3.198 (* return an existing interpretation *)
3.199 SOME (intr, model, args)
3.200 @@ -1727,7 +1730,7 @@
3.201 let
3.202 val index = #index info
3.203 val descr = #descr info
3.204 - val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
3.205 + val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
3.206 val typ_assoc = dtyps ~~ Ts'
3.207 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
3.208 val _ = (if Library.exists (fn d =>
3.209 @@ -1751,8 +1754,9 @@
3.210 val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type (s', Ts')))
3.211 val total = size_of_type i
3.212 (* int option -- only recursive IDTs have an associated depth *)
3.213 - val depth = assoc (typs, Type (s', Ts'))
3.214 - val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
3.215 + val depth = AList.lookup (op =) typs (Type (s', Ts'))
3.216 + val typs' = (case depth of NONE => typs | SOME n =>
3.217 + AList.update (op =) (Type (s', Ts'), n-1) typs)
3.218 (* returns an interpretation where everything is mapped to "undefined" *)
3.219 (* DatatypeAux.dtyp list -> interpretation *)
3.220 fun make_undef [] =
3.221 @@ -1904,7 +1908,7 @@
3.222 let
3.223 val index = #index info
3.224 val descr = #descr info
3.225 - val (dtname, dtyps, _) = (valOf o assoc) (descr, index)
3.226 + val (dtname, dtyps, _) = (the o AList.lookup (op =) descr) index
3.227 (* number of all constructors, including those of different *)
3.228 (* (mutually recursive) datatypes within the same descriptor 'descr' *)
3.229 val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs) descr)
3.230 @@ -1995,7 +1999,7 @@
3.231 SOME args => (n, args)
3.232 | NONE => get_cargs_rec (n+1, xs))
3.233 in
3.234 - get_cargs_rec (0, (valOf o assoc) (mc_intrs, idx))
3.235 + get_cargs_rec (0, (the o AList.lookup (op =) mc_intrs) idx)
3.236 end
3.237 (* returns the number of constructors in datatypes that occur in *)
3.238 (* the descriptor 'descr' before the datatype given by 'idx' *)
3.239 @@ -2015,7 +2019,7 @@
3.240 (* where 'idx' gives the datatype and 'elem' the element of it *)
3.241 (* int -> int -> interpretation *)
3.242 fun compute_array_entry idx elem =
3.243 - case Array.sub ((valOf o assoc) (INTRS, idx), elem) of
3.244 + case Array.sub ((the o AList.lookup (op =) INTRS) idx, elem) of
3.245 SOME result =>
3.246 (* simply return the previously computed result *)
3.247 result
3.248 @@ -2033,7 +2037,7 @@
3.249 (* select the correct subtree of the parameter corresponding to constructor 'c' *)
3.250 val p_intr = select_subtree (List.nth (p_intrs, get_coffset idx + c), args)
3.251 (* find the indices of the constructor's recursive arguments *)
3.252 - val (_, _, constrs) = (valOf o assoc) (descr, idx)
3.253 + val (_, _, constrs) = (the o AList.lookup (op =) descr) idx
3.254 val constr_args = (snd o List.nth) (constrs, c)
3.255 val rec_args = List.filter (DatatypeAux.is_rec_type o fst) (constr_args ~~ args)
3.256 val rec_args' = map (fn (dtyp, elem) => (DatatypeAux.dest_DtRec dtyp, elem)) rec_args
3.257 @@ -2041,7 +2045,7 @@
3.258 val result = foldl (fn ((idx, elem), intr) =>
3.259 interpretation_apply (intr, compute_array_entry idx elem)) p_intr rec_args'
3.260 (* update 'INTRS' *)
3.261 - val _ = Array.update ((valOf o assoc) (INTRS, idx), elem, SOME result)
3.262 + val _ = Array.update ((the o AList.lookup (op =) INTRS) idx, elem, SOME result)
3.263 in
3.264 result
3.265 end
3.266 @@ -2060,13 +2064,13 @@
3.267 in
3.268 modifyi_loop 0
3.269 end
3.270 - val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index))
3.271 + val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((the o AList.lookup (op =) INTRS) index)
3.272 (* 'a Array.array -> 'a list *)
3.273 fun toList arr =
3.274 Array.foldr op:: [] arr
3.275 in
3.276 (* return the part of 'INTRS' that corresponds to the current datatype *)
3.277 - SOME ((Node o (map valOf) o toList o valOf o assoc) (INTRS, index), model', args')
3.278 + SOME ((Node o map the o toList o the o AList.lookup (op =) INTRS) index, model', args')
3.279 end
3.280 end
3.281 else
3.282 @@ -2515,7 +2519,7 @@
3.283 val (typs, _) = model
3.284 val index = #index info
3.285 val descr = #descr info
3.286 - val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
3.287 + val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
3.288 val typ_assoc = dtyps ~~ Ts
3.289 (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
3.290 val _ = (if Library.exists (fn d =>
4.1 --- a/src/HOL/ex/SVC_Oracle.ML Thu Sep 08 16:08:50 2005 +0200
4.2 +++ b/src/HOL/ex/SVC_Oracle.ML Thu Sep 08 16:09:23 2005 +0200
4.3 @@ -38,7 +38,7 @@
4.4 case t of
4.5 Free _ => t (*but not existing Vars, lest the names clash*)
4.6 | Bound _ => t
4.7 - | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
4.8 + | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
4.9 SOME v => v
4.10 | NONE => insert t)
4.11 (*abstraction of a numeric literal*)
5.1 --- a/src/Pure/Isar/context_rules.ML Thu Sep 08 16:08:50 2005 +0200
5.2 +++ b/src/Pure/Isar/context_rules.ML Thu Sep 08 16:09:23 2005 +0200
5.3 @@ -111,7 +111,7 @@
5.4 fun print_rules prt x (Rules {rules, ...}) =
5.5 let
5.6 fun prt_kind (i, b) =
5.7 - Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
5.8 + Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
5.9 (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
5.10 (sort (int_ord o pairself fst) rules));
5.11 in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
6.1 --- a/src/Pure/Isar/method.ML Thu Sep 08 16:08:50 2005 +0200
6.2 +++ b/src/Pure/Isar/method.ML Thu Sep 08 16:09:23 2005 +0200
6.3 @@ -383,7 +383,7 @@
6.4 val params = rev(Term.rename_wrt_term Bi params)
6.5 (* as they are printed: bound variables with *)
6.6 (* the same name are renamed during printing *)
6.7 - fun types' (a, ~1) = (case assoc (params, a) of
6.8 + fun types' (a, ~1) = (case AList.lookup (op =) params a of
6.9 NONE => types (a, ~1)
6.10 | some => some)
6.11 | types' xi = types xi;
7.1 --- a/src/Pure/Syntax/parser.ML Thu Sep 08 16:08:50 2005 +0200
7.2 +++ b/src/Pure/Syntax/parser.ML Thu Sep 08 16:09:23 2005 +0200
7.3 @@ -724,7 +724,7 @@
7.4 (_, _, _, Nonterminal (nt, minPrec) :: _, _, _) =>
7.5 let (*predictor operation*)
7.6 val (used', new_states) =
7.7 - (case assoc (used, nt) of
7.8 + (case AList.lookup (op =) used nt of
7.9 SOME (usedPrec, l) => (*nonterminal has been processed*)
7.10 if usedPrec <= minPrec then
7.11 (*wanted precedence has been processed*)
8.1 --- a/src/Pure/Syntax/syntax.ML Thu Sep 08 16:08:50 2005 +0200
8.2 +++ b/src/Pure/Syntax/syntax.ML Thu Sep 08 16:09:23 2005 +0200
8.3 @@ -110,7 +110,7 @@
8.4 fun lookup_tokentr tabs modes =
8.5 let val trs = gen_distinct eq_fst
8.6 (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
8.7 - in fn c => Option.map fst (assoc (trs, c)) end;
8.8 + in fn c => Option.map fst (AList.lookup (op =) trs c) end;
8.9
8.10 fun merge_tokentrtabs tabs1 tabs2 =
8.11 let
9.1 --- a/src/Pure/proof_general.ML Thu Sep 08 16:08:50 2005 +0200
9.2 +++ b/src/Pure/proof_general.ML Thu Sep 08 16:09:23 2005 +0200
9.3 @@ -1116,12 +1116,12 @@
9.4 fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
9.5
9.6 fun setpref name value =
9.7 - (case assoc (allprefs(), name) of
9.8 + (case AList.lookup (op =) (allprefs ()) name of
9.9 NONE => warning ("Unknown pref: " ^ quote name)
9.10 | SOME (_, (_, _, set)) => set value);
9.11
9.12 fun getpref name =
9.13 - (case assoc (allprefs(), name) of
9.14 + (case AList.lookup (op =) (allprefs ()) name of
9.15 NONE => warning ("Unknown pref: " ^ quote name)
9.16 | SOME (_, (_, (_,get), _)) =>
9.17 issue_pgip "prefval" [("name", name)] (get ()));
9.18 @@ -1164,7 +1164,7 @@
9.19 (* Proof control commands *)
9.20
9.21 local
9.22 - fun xmlattro attr attrs = assoc(attrs,attr)
9.23 + fun xmlattro attr attrs = AList.lookup (op =) attrs attr
9.24
9.25 fun xmlattr attr attrs =
9.26 (case xmlattro attr attrs of
10.1 --- a/src/Pure/proofterm.ML Thu Sep 08 16:08:50 2005 +0200
10.2 +++ b/src/Pure/proofterm.ML Thu Sep 08 16:09:23 2005 +0200
10.3 @@ -470,7 +470,7 @@
10.4 (**** Freezing and thawing of variables in proof terms ****)
10.5
10.6 fun frzT names =
10.7 - map_type_tvar (fn (ixn, xs) => TFree (valOf (assoc (names, ixn)), xs));
10.8 + map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs));
10.9
10.10 fun thawT names =
10.11 map_type_tfree (fn (s, xs) => case assoc (names, s) of
10.12 @@ -484,7 +484,7 @@
10.13 | freeze names names' (Const (s, T)) = Const (s, frzT names' T)
10.14 | freeze names names' (Free (s, T)) = Free (s, frzT names' T)
10.15 | freeze names names' (Var (ixn, T)) =
10.16 - Free (valOf (assoc (names, ixn)), frzT names' T)
10.17 + Free (the (assoc (names, ixn)), frzT names' T)
10.18 | freeze names names' t = t;
10.19
10.20 fun thaw names names' (t $ u) =
10.21 @@ -553,7 +553,7 @@
10.22 val ixns = add_term_tvar_ixns (t, []);
10.23 val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
10.24 fun thaw (f as (a, S)) =
10.25 - (case gen_assoc (op =) (fmap, f) of
10.26 + (case AList.lookup (op =) fmap f of
10.27 NONE => TFree f
10.28 | SOME b => TVar ((b, 0), S));
10.29 in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
10.30 @@ -810,8 +810,9 @@
10.31 | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
10.32 and add_npvars' Ts (vs, t) = (case strip_comb t of
10.33 (Var (ixn, _), ts) => if test_args [] ts then vs
10.34 - else Library.foldl (add_npvars' Ts) (overwrite (vs,
10.35 - (ixn, Library.foldl (add_funvars Ts) (getOpt (assoc (vs, ixn), []), ts))), ts)
10.36 + else Library.foldl (add_npvars' Ts)
10.37 + (AList.update (op =) (ixn,
10.38 + Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts)
10.39 | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
10.40 | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
10.41
11.1 --- a/src/Pure/term.ML Thu Sep 08 16:08:50 2005 +0200
11.2 +++ b/src/Pure/term.ML Thu Sep 08 16:09:23 2005 +0200
11.3 @@ -861,7 +861,7 @@
11.4 fun subst_free [] = (fn t=>t)
11.5 | subst_free pairs =
11.6 let fun substf u =
11.7 - case gen_assoc (op aconv) (pairs, u) of
11.8 + case AList.lookup (op aconv) pairs u of
11.9 SOME u' => u'
11.10 | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
11.11 | t$u' => substf t $ substf u'
11.12 @@ -916,7 +916,7 @@
11.13 let
11.14 fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
11.15 | subst (t $ u) = subst t $ subst u
11.16 - | subst t = if_none (gen_assoc (op aconv) (inst, t)) t;
11.17 + | subst t = if_none (AList.lookup (op aconv) inst t) t;
11.18 in subst tm end;
11.19
11.20 (*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*)
11.21 @@ -924,7 +924,7 @@
11.22 | typ_subst_atomic inst ty =
11.23 let
11.24 fun subst (Type (a, Ts)) = Type (a, map subst Ts)
11.25 - | subst T = if_none (gen_assoc (op = : typ * typ -> bool) (inst, T)) T;
11.26 + | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
11.27 in subst ty end;
11.28
11.29 fun subst_atomic_types [] tm = tm
11.30 @@ -977,7 +977,7 @@
11.31 let
11.32 fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
11.33 | subst_typ (TVar v) =
11.34 - (case gen_assoc eq_tvar (instT, v) of
11.35 + (case AList.lookup eq_tvar instT v of
11.36 SOME T => T
11.37 | NONE => raise SAME)
11.38 | subst_typ _ = raise SAME
11.39 @@ -995,7 +995,7 @@
11.40 | subst (Free (x, T)) = Free (x, substT T)
11.41 | subst (Var (xi, T)) =
11.42 let val (T', same) = (substT T, false) handle SAME => (T, true) in
11.43 - (case gen_assoc eq_var (inst, (xi, T')) of
11.44 + (case AList.lookup eq_var inst (xi, T') of
11.45 SOME t => t
11.46 | NONE => if same then raise SAME else Var (xi, T'))
11.47 end
12.1 --- a/src/ZF/Tools/induct_tacs.ML Thu Sep 08 16:08:50 2005 +0200
12.2 +++ b/src/ZF/Tools/induct_tacs.ML Thu Sep 08 16:09:23 2005 +0200
12.3 @@ -84,7 +84,7 @@
12.4 | mk_pair _ = raise Match
12.5 val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
12.6 (#2 (strip_context Bi))
12.7 - in case assoc (pairs, var) of
12.8 + in case AList.lookup (op =) pairs var of
12.9 NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
12.10 | SOME t => t
12.11 end;
13.1 --- a/src/ZF/Tools/inductive_package.ML Thu Sep 08 16:08:50 2005 +0200
13.2 +++ b/src/ZF/Tools/inductive_package.ML Thu Sep 08 16:09:23 2005 +0200
13.3 @@ -300,7 +300,7 @@
13.4 prem is a premise of an intr rule*)
13.5 fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
13.6 (Const("op :",_)$t$X), iprems) =
13.7 - (case gen_assoc (op aconv) (ind_alist, X) of
13.8 + (case AList.lookup (op aconv) ind_alist X of
13.9 SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
13.10 | NONE => (*possibly membership in M(rec_tm), for M monotone*)
13.11 let fun mk_sb (rec_tm,pred) =
13.12 @@ -314,7 +314,7 @@
13.13 val iprems = foldr (add_induct_prem ind_alist) []
13.14 (Logic.strip_imp_prems intr)
13.15 val (t,X) = Ind_Syntax.rule_concl intr
13.16 - val (SOME pred) = gen_assoc (op aconv) (ind_alist, X)
13.17 + val (SOME pred) = AList.lookup (op aconv) ind_alist X
13.18 val concl = FOLogic.mk_Trueprop (pred $ t)
13.19 in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
13.20 handle Bind => error"Recursion term not found in conclusion";
14.1 --- a/src/ZF/Tools/primrec_package.ML Thu Sep 08 16:08:50 2005 +0200
14.2 +++ b/src/ZF/Tools/primrec_package.ML Thu Sep 08 16:09:23 2005 +0200
14.3 @@ -80,7 +80,7 @@
14.4 else case rec_fn_opt of
14.5 NONE => SOME (fname, ftype, ls, rs, con_info, [new_eqn])
14.6 | SOME (fname', _, ls', rs', con_info': constructor_info, eqns) =>
14.7 - if isSome (assoc (eqns, cname)) then
14.8 + if AList.defined (op =) eqns cname then
14.9 raise RecError "constructor already occurred as pattern"
14.10 else if (ls <> ls') orelse (rs <> rs') then
14.11 raise RecError "non-recursive arguments are inconsistent"
14.12 @@ -120,7 +120,7 @@
14.13 Missing cases are replaced by 0 and all cases are put into order.*)
14.14 fun add_case ((cname, recursor_pair), cases) =
14.15 let val (rhs, recursor_rhs, eq) =
14.16 - case assoc (eqns, cname) of
14.17 + case AList.lookup (op =) eqns cname of
14.18 NONE => (warning ("no equation for constructor " ^ cname ^
14.19 "\nin definition of function " ^ fname);
14.20 (Const ("0", Ind_Syntax.iT),