--- a/src/Provers/blast.ML Tue Sep 06 08:29:17 2005 +0200
+++ b/src/Provers/blast.ML Tue Sep 06 08:30:43 2005 +0200
@@ -171,7 +171,7 @@
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts)
| fromType alist (Term.TFree(a,_)) = Free a
| fromType alist (Term.TVar (ixn,_)) =
- (case (assoc_string_int(!alist,ixn)) of
+ (case (AList.lookup (op =) (!alist) ixn) of
NONE => let val t' = Var(ref NONE)
in alist := (ixn, t') :: !alist; t'
end
@@ -381,7 +381,7 @@
| from (Term.Free (a,_)) = Free a
| from (Term.Bound i) = Bound i
| from (Term.Var (ixn,T)) =
- (case (assoc_string_int(!alistVar,ixn)) of
+ (case (AList.lookup (op =) (!alistVar) ixn) of
NONE => let val t' = Var(ref NONE)
in alistVar := (ixn, t') :: !alistVar; t'
end
@@ -1214,7 +1214,7 @@
| Term.Free (a,_) => apply (Free a)
| Term.Bound i => apply (Bound i)
| Term.Var (ix,_) =>
- (case (assoc_string_int(!alistVar,ix)) of
+ (case (AList.lookup (op =) (!alistVar) ix) of
NONE => (alistVar := (ix, (ref NONE, bounds ts))
:: !alistVar;
Var (hdvar(!alistVar)))
--- a/src/Pure/Isar/locale.ML Tue Sep 06 08:29:17 2005 +0200
+++ b/src/Pure/Isar/locale.ML Tue Sep 06 08:30:43 2005 +0200
@@ -625,7 +625,7 @@
(* ren maps names to (new) names and syntax; represented as association list *)
fun rename_var ren (x, mx) =
- case assoc_string (ren, x) of
+ case AList.lookup (op =) ren x of
NONE => (x, mx)
| SOME (x', NONE) =>
(x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*)
@@ -635,7 +635,7 @@
else (x', SOME mx'); (*change syntax*)
fun rename ren x =
- case assoc_string (ren, x) of
+ case AList.lookup (op =) ren x of
NONE => x
| SOME (x', _) => x'; (*ignore syntax*)
@@ -1391,9 +1391,9 @@
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
- (x, assoc_string (parms, x), mx)) fixes)
+ (x, AList.lookup (op =) parms x, mx)) fixes)
| finish_ext_elem parms _ (Constrains csts, _) =
- Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts)
+ Constrains (map (fn (x, _) => (x, (the o AList.lookup (op =) parms) x)) csts)
| finish_ext_elem _ close (Assumes asms, propp) =
close (Assumes (map #1 asms ~~ propp))
| finish_ext_elem _ close (Defines defs, propp) =
--- a/src/Pure/Proof/extraction.ML Tue Sep 06 08:29:17 2005 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Sep 06 08:30:43 2005 +0200
@@ -532,7 +532,7 @@
(Bound (length Us), eT :: Us);
val u = list_comb (incr_boundvars (length Us') t,
map Bound (length Us - 1 downto 0));
- val u' = (case assoc_string (types, tname_of T) of
+ val u' = (case AList.lookup (op =) types (tname_of T) of
SOME ((_, SOME f)) => f r eT u T
| _ => Const ("realizes", eT --> T --> T) $ r $ u)
in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
--- a/src/Pure/tactic.ML Tue Sep 06 08:29:17 2005 +0200
+++ b/src/Pure/tactic.ML Tue Sep 06 08:30:43 2005 +0200
@@ -240,7 +240,7 @@
let val thy = Thm.theory_of_thm st
and params = params_of_state st i
and rts = types_sorts rule and (types,sorts) = types_sorts st
- fun types'(a, ~1) = (case assoc_string (params, a) of NONE => types (a, ~1) | sm => sm)
+ fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
| types' ixn = types ixn;
val used = Drule.add_used rule (Drule.add_used st []);
in read_insts thy rts (types',sorts) used sinsts end;
@@ -666,7 +666,7 @@
val frees = map Term.dest_Free (Term.term_frees statement);
val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
- val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
+ val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
fun err msg = raise ERROR_MESSAGE
(msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
--- a/src/Pure/term.ML Tue Sep 06 08:29:17 2005 +0200
+++ b/src/Pure/term.ML Tue Sep 06 08:30:43 2005 +0200
@@ -736,7 +736,7 @@
let
val ren = match_bvs (pat, obj, []);
fun ren_abs (Abs (x, T, b)) =
- Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b)
+ Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b)
| ren_abs (f $ t) = ren_abs f $ ren_abs t
| ren_abs t = t
in if null ren then NONE else SOME (ren_abs t) end;
@@ -934,7 +934,7 @@
| typ_subst_TVars inst ty =
let
fun subst (Type (a, Ts)) = Type (a, map subst Ts)
- | subst (T as TVar (xi, _)) = if_none (assoc_string_int (inst, xi)) T
+ | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T
| subst T = T;
in subst ty end;
@@ -945,7 +945,7 @@
fun subst_Vars [] tm = tm
| subst_Vars inst tm =
let
- fun subst (t as Var (xi, _)) = if_none (assoc_string_int (inst, xi)) t
+ fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t
| subst (Abs (a, T, t)) = Abs (a, T, subst t)
| subst (t $ u) = subst t $ subst u
| subst t = t;
@@ -959,7 +959,7 @@
fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
| subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
| subst (t as Var (xi, T)) =
- (case assoc_string_int (inst, xi) of
+ (case AList.lookup (op =) inst xi of
NONE => Var (xi, typ_subst_TVars instT T)
| SOME t => t)
| subst (t as Bound _) = t
--- a/src/Pure/type_infer.ML Tue Sep 06 08:29:17 2005 +0200
+++ b/src/Pure/type_infer.ML Tue Sep 06 08:30:43 2005 +0200
@@ -111,7 +111,7 @@
fun pretyp_of is_param (params, typ) =
let
fun add_parms (TVar (xi as (x, _), S)) ps =
- if is_param xi andalso is_none (assoc_string_int (ps, xi))
+ if is_param xi andalso is_none (AList.lookup (op =) ps xi)
then (xi, mk_param S) :: ps else ps
| add_parms (TFree _) ps = ps
| add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
@@ -119,7 +119,7 @@
val params' = add_parms typ params;
fun pre_of (TVar (v as (xi, _))) =
- (case assoc_string_int (params', xi) of
+ (case AList.lookup (op =) params' xi of
NONE => PTVar v
| SOME p => p)
| pre_of (TFree ("'_dummy_", S)) = mk_param S
@@ -137,7 +137,7 @@
fun preterm_of const_type is_param ((vparams, params), tm) =
let
fun add_vparm (ps, xi) =
- if is_none (assoc_string_int (ps, xi)) then
+ if is_none (AList.lookup (op =) ps xi) then
(xi, mk_param []) :: ps
else ps;
@@ -149,7 +149,7 @@
| add_vparms (ps, _) = ps;
val vparams' = add_vparms (vparams, tm);
- fun var_param xi = the (assoc_string_int (vparams', xi));
+ fun var_param xi = (the o AList.lookup (op =) vparams') xi;
val preT_of = pretyp_of is_param;
@@ -457,7 +457,7 @@
^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
fun get xi =
- (case (assoc_string_int (env, xi), def_sort xi) of
+ (case (AList.lookup (op =) env xi, def_sort xi) of
(NONE, NONE) => Type.defaultS tsig
| (NONE, SOME S) => S
| (SOME S, NONE) => S