introduced AList module
authorhaftmann
Mon Sep 19 16:38:35 2005 +0200 (2005-09-19)
changeset 17485c39871c52977
parent 17484 f6a225f97f0a
child 17486 d691bf893d9f
introduced AList module
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Mon Sep 19 15:12:13 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Mon Sep 19 16:38:35 2005 +0200
     1.3 @@ -483,13 +483,13 @@
     1.4  
     1.5  fun evalc_atom at = case at of  
     1.6    (Const (p,_) $ s $ t) =>
     1.7 -   ( case assoc (operations,p) of 
     1.8 +   ( case AList.lookup (op =) operations p of 
     1.9      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
    1.10                  else HOLogic.false_const)  
    1.11      handle _ => at) 
    1.12        | _ =>  at) 
    1.13        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    1.14 -  case assoc (operations,p) of 
    1.15 +  case AList.lookup (op =) operations p of 
    1.16      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
    1.17                 then HOLogic.false_const else HOLogic.true_const)  
    1.18      handle _ => at) 
     2.1 --- a/src/HOL/Integ/cooper_proof.ML	Mon Sep 19 15:12:13 2005 +0200
     2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Mon Sep 19 16:38:35 2005 +0200
     2.3 @@ -787,7 +787,7 @@
     2.4  
     2.5  fun rho_for_evalc sg at = case at of  
     2.6      (Const (p,_) $ s $ t) =>(  
     2.7 -    case assoc (operations,p) of 
     2.8 +    case AList.lookup (op =) operations p of 
     2.9          SOME f => 
    2.10             ((if (f ((dest_numeral s),(dest_numeral t))) 
    2.11               then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
    2.12 @@ -795,7 +795,7 @@
    2.13  		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
    2.14          | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
    2.15       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    2.16 -       case assoc (operations,p) of 
    2.17 +       case AList.lookup (op =) operations p of 
    2.18           SOME f => 
    2.19             ((if (f ((dest_numeral s),(dest_numeral t))) 
    2.20               then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
     3.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Sep 19 15:12:13 2005 +0200
     3.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Sep 19 16:38:35 2005 +0200
     3.3 @@ -483,13 +483,13 @@
     3.4  
     3.5  fun evalc_atom at = case at of  
     3.6    (Const (p,_) $ s $ t) =>
     3.7 -   ( case assoc (operations,p) of 
     3.8 +   ( case AList.lookup (op =) operations p of 
     3.9      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
    3.10                  else HOLogic.false_const)  
    3.11      handle _ => at) 
    3.12        | _ =>  at) 
    3.13        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    3.14 -  case assoc (operations,p) of 
    3.15 +  case AList.lookup (op =) operations p of 
    3.16      SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
    3.17                 then HOLogic.false_const else HOLogic.true_const)  
    3.18      handle _ => at) 
     4.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Sep 19 15:12:13 2005 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Sep 19 16:38:35 2005 +0200
     4.3 @@ -787,7 +787,7 @@
     4.4  
     4.5  fun rho_for_evalc sg at = case at of  
     4.6      (Const (p,_) $ s $ t) =>(  
     4.7 -    case assoc (operations,p) of 
     4.8 +    case AList.lookup (op =) operations p of 
     4.9          SOME f => 
    4.10             ((if (f ((dest_numeral s),(dest_numeral t))) 
    4.11               then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
    4.12 @@ -795,7 +795,7 @@
    4.13  		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
    4.14          | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
    4.15       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    4.16 -       case assoc (operations,p) of 
    4.17 +       case AList.lookup (op =) operations p of 
    4.18           SOME f => 
    4.19             ((if (f ((dest_numeral s),(dest_numeral t))) 
    4.20               then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
     5.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Sep 19 15:12:13 2005 +0200
     5.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Sep 19 16:38:35 2005 +0200
     5.3 @@ -196,9 +196,7 @@
     5.4  fun mk_Free s T i = Free (s ^ (string_of_int i), T);
     5.5  
     5.6  fun subst_DtTFree _ substs (T as (DtTFree name)) =
     5.7 -      (case assoc (substs, name) of
     5.8 -         NONE => T
     5.9 -       | SOME U => U)
    5.10 +      AList.lookup (op =) substs name |> the_default T
    5.11    | subst_DtTFree i substs (DtType (name, ts)) =
    5.12        DtType (name, map (subst_DtTFree i substs) ts)
    5.13    | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
    5.14 @@ -236,15 +234,15 @@
    5.15  fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
    5.16    | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
    5.17    | dtyp_of_typ new_dts (Type (tname, Ts)) =
    5.18 -      (case assoc (new_dts, tname) of
    5.19 +      (case AList.lookup (op =) new_dts tname of
    5.20           NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
    5.21         | SOME vs => if map (try dest_TFree) Ts = map SOME vs then
    5.22               DtRec (find_index (curry op = tname o fst) new_dts)
    5.23             else error ("Illegal occurence of recursive type " ^ tname));
    5.24  
    5.25 -fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, valOf (assoc (sorts, a)))
    5.26 +fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, (the o AList.lookup (op =) sorts) a)
    5.27    | typ_of_dtyp descr sorts (DtRec i) =
    5.28 -      let val (s, ds, _) = valOf (assoc (descr, i))
    5.29 +      let val (s, ds, _) = (the o AList.lookup (op =) descr) i
    5.30        in Type (s, map (typ_of_dtyp descr sorts) ds) end
    5.31    | typ_of_dtyp descr sorts (DtType (s, ds)) =
    5.32        Type (s, map (typ_of_dtyp descr sorts) ds);
    5.33 @@ -279,7 +277,7 @@
    5.34      val descr' = List.concat descr;
    5.35      fun is_nonempty_dt is i =
    5.36        let
    5.37 -        val (_, _, constrs) = valOf (assoc (descr', i));
    5.38 +        val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
    5.39          fun arg_nonempty (_, DtRec i) = if i mem is then false
    5.40                else is_nonempty_dt (i::is) i
    5.41            | arg_nonempty _ = true;
    5.42 @@ -303,7 +301,7 @@
    5.43           NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
    5.44             \ nested recursion")
    5.45         | (SOME {index, descr, ...}) =>
    5.46 -           let val (_, vars, _) = valOf (assoc (descr, index));
    5.47 +           let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
    5.48                 val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths =>
    5.49                   typ_error T ("Type constructor " ^ tname ^ " used with wrong\
    5.50                    \ number of arguments")
     6.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 19 15:12:13 2005 +0200
     6.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 19 16:38:35 2005 +0200
     6.3 @@ -228,12 +228,12 @@
     6.4        p :: prod_factors (1::p) t @ prod_factors (2::p) u
     6.5    | prod_factors p _ = [];
     6.6  
     6.7 -fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
     6.8 +fun mg_prod_factors ts (t $ u) fs = if t mem ts then
     6.9          let val f = prod_factors [] u
    6.10          in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
    6.11 -      else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
    6.12 -  | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
    6.13 -  | mg_prod_factors ts (fs, _) = fs;
    6.14 +      else mg_prod_factors ts u (mg_prod_factors ts t fs)
    6.15 +  | mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs
    6.16 +  | mg_prod_factors ts _ fs = fs;
    6.17  
    6.18  fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
    6.19        if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
    6.20 @@ -265,11 +265,11 @@
    6.21  val remove_split = rewrite_rule [split_conv RS eq_reflection];
    6.22  
    6.23  fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
    6.24 -  rl (mg_prod_factors vs ([], Thm.prop_of rl))));
    6.25 +  rl (mg_prod_factors vs (Thm.prop_of rl) [])));
    6.26  
    6.27  fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
    6.28    rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
    6.29 -      Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
    6.30 +      Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl)))));
    6.31  
    6.32  
    6.33  (** process rules **)
    6.34 @@ -377,7 +377,7 @@
    6.35        let
    6.36          val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
    6.37  
    6.38 -        val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
    6.39 +        val pred_of = AList.lookup (op aconv) (cs ~~ preds);
    6.40  
    6.41          fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
    6.42                (case pred_of u of
    6.43 @@ -408,13 +408,13 @@
    6.44  
    6.45      val ind_prems = map mk_ind_prem intr_ts;
    6.46  
    6.47 -    val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems);
    6.48 +    val factors = Library.fold (mg_prod_factors preds) ind_prems [];
    6.49  
    6.50      (* make conclusions for induction rules *)
    6.51  
    6.52      fun mk_ind_concl ((c, P), (ts, x)) =
    6.53        let val T = HOLogic.dest_setT (fastype_of c);
    6.54 -          val ps = getOpt (assoc (factors, P), []);
    6.55 +          val ps = AList.lookup (op =) factors P |> the_default [];
    6.56            val Ts = prodT_factors [] ps T;
    6.57            val (frees, x') = foldr (fn (T', (fs, s)) =>
    6.58              ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 19 15:12:13 2005 +0200
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Sep 19 16:38:35 2005 +0200
     7.3 @@ -112,7 +112,7 @@
     7.4      val rname = space_implode "_" (s ^ "R" :: vs);
     7.5  
     7.6      fun mk_Tprem n v =
     7.7 -      let val SOME T = assoc (rvs, v)
     7.8 +      let val T = (the o AList.lookup (op =) rvs) v
     7.9        in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
    7.10          Extraction.mk_typ (if n then Extraction.nullT
    7.11            else TVar (("'" ^ v, 0), HOLogic.typeS)))
    7.12 @@ -226,7 +226,7 @@
    7.13        val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
    7.14        fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
    7.15        val r' = list_abs_free (List.mapPartial (fn intr =>
    7.16 -        Option.map (pair (name_of_fn intr)) (assoc (frees, name_of_fn intr))) intrs,
    7.17 +        Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
    7.18            if length concls = 1 then r $ x else r)
    7.19      in
    7.20        if length concls = 1 then lambda x r' else r'
    7.21 @@ -253,7 +253,7 @@
    7.22      val xs = rev (Term.add_vars (prop_of rule) []);
    7.23      val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
    7.24      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    7.25 -    val vs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rlzvs, ixn)))) xs;
    7.26 +    val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
    7.27      val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
    7.28  
    7.29      fun mk_prf _ [] prf = prf
    7.30 @@ -270,12 +270,15 @@
    7.31        (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
    7.32    end;
    7.33  
    7.34 -fun add_rule (rss, r) =
    7.35 +fun add_rule r rss =
    7.36    let
    7.37      val _ $ (_ $ _ $ S) = concl_of r;
    7.38      val (Const (s, _), _) = strip_comb S;
    7.39 -    val rs = getOpt (assoc (rss, s), []);
    7.40 -  in AList.update (op =) (s, rs @ [r]) rss end;
    7.41 +  in
    7.42 +    rss
    7.43 +    |> AList.default (op =) (s, [])
    7.44 +    |> AList.map_entry (op =) s (fn rs => rs @ [r])
    7.45 +  end;
    7.46  
    7.47  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    7.48    let
    7.49 @@ -284,7 +287,7 @@
    7.50      val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
    7.51      val (_, params) = strip_comb S;
    7.52      val params' = map dest_Var params;
    7.53 -    val rss = Library.foldl add_rule ([], intrs);
    7.54 +    val rss = [] |> Library.fold add_rule intrs;
    7.55      val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
    7.56      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    7.57  
     8.1 --- a/src/HOL/Tools/record_package.ML	Mon Sep 19 15:12:13 2005 +0200
     8.2 +++ b/src/HOL/Tools/record_package.ML	Mon Sep 19 16:38:35 2005 +0200
     8.3 @@ -2054,7 +2054,7 @@
     8.4      (* args *)
     8.5  
     8.6      val defaultS = Sign.defaultS sign;
     8.7 -    val args = map (fn x => (x, getOpt (assoc (envir, x), defaultS))) params;
     8.8 +    val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
     8.9  
    8.10  
    8.11      (* errors *)
     9.1 --- a/src/Pure/Isar/locale.ML	Mon Sep 19 15:12:13 2005 +0200
     9.2 +++ b/src/Pure/Isar/locale.ML	Mon Sep 19 16:38:35 2005 +0200
     9.3 @@ -205,7 +205,7 @@
     9.4            else thm |> Drule.implies_intr_list (map cert hyps)
     9.5              |> Drule.tvars_intr_list (map #1 tinst')
     9.6              |> (fn (th, al) => th |> Thm.instantiate
     9.7 -                ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
     9.8 +                ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'),
     9.9                    []))
    9.10              |> (fn th => Drule.implies_elim_list th
    9.11                   (map (Thm.assume o cert o tinst_tab_term tinst) hyps))
    9.12 @@ -251,7 +251,7 @@
    9.13            else thm |> Drule.implies_intr_list (map cert hyps)
    9.14              |> Drule.tvars_intr_list (map #1 tinst')
    9.15              |> (fn (th, al) => th |> Thm.instantiate
    9.16 -                ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
    9.17 +                ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'),
    9.18                    []))
    9.19              |> Drule.forall_intr_list (map (cert o #1) inst')
    9.20              |> Drule.forall_elim_list (map (cert o #2) inst') 
    9.21 @@ -691,7 +691,7 @@
    9.22  (* type instantiation *)
    9.23  
    9.24  fun inst_type [] T = T
    9.25 -  | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;
    9.26 +  | inst_type env T = Term.map_type_tfree (fn v => AList.lookup (op =) env v |> the_default (TFree v)) T;
    9.27  
    9.28  fun inst_term [] t = t
    9.29    | inst_term env t = Term.map_term_types (inst_type env) t;
    9.30 @@ -713,7 +713,7 @@
    9.31            |> Drule.tvars_intr_list (map (#1 o #1) env')
    9.32            |> (fn (th', al) => th' |>
    9.33              Thm.instantiate ((map (fn ((a, _), T) =>
    9.34 -              (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), []))
    9.35 +              (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) env'), []))
    9.36            |> (fn th'' => Drule.implies_elim_list th''
    9.37                (map (Thm.assume o cert o inst_term env') hyps))
    9.38        end;
    9.39 @@ -941,7 +941,7 @@
    9.40                ((name, map (rename ren) ps), ths)) regs;
    9.41            val new_regs = gen_rems eq_fst (regs', ids);
    9.42            val new_ids = map fst new_regs;
    9.43 -          val new_idTs = map (apsnd (map (fn p => (p, valOf (assoc (ps, p)))))) new_ids;
    9.44 +          val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
    9.45  
    9.46            val new_ths = map (fn (_, ths') =>
    9.47                map (Drule.satisfy_hyps ths o rename_thm ren o inst_thm ctxt env) ths') new_regs;
    9.48 @@ -1048,7 +1048,7 @@
    9.49      val all_params' = params_of' elemss;
    9.50      val all_params = param_types all_params';
    9.51      val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
    9.52 -         (((name, map (fn p => (p, assoc (all_params, p))) ps), mode), elems))
    9.53 +         (((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems))
    9.54           elemss;
    9.55      fun inst_th th = let
    9.56           val {hyps, prop, ...} = Thm.rep_thm th;
    9.57 @@ -1423,7 +1423,7 @@
    9.58     If so, which are these??? *)
    9.59  
    9.60  fun finish_parms parms (((name, ps), mode), elems) =
    9.61 -  (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), mode), elems);
    9.62 +  (((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems);
    9.63  
    9.64  fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
    9.65        let
    9.66 @@ -1582,7 +1582,7 @@
    9.67        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
    9.68      (* replace extended ids (for axioms) by ids *)
    9.69      val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
    9.70 -        (((n, map (fn p => (p, assoc (ps', p) |> valOf)) ps), mode), elems))
    9.71 +        (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
    9.72        (ids ~~ all_elemss);
    9.73  
    9.74      (* CB: all_elemss and parms contain the correct parameter types *)
    9.75 @@ -2229,7 +2229,7 @@
    9.76      val (given_ps, given_insts) = split_list given;
    9.77      val tvars = foldr Term.add_typ_tvars [] pvTs;
    9.78      val used = foldr Term.add_typ_varnames [] pvTs;
    9.79 -    fun sorts (a, i) = assoc (tvars, (a, i));
    9.80 +    fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
    9.81      val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
    9.82      val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
    9.83      val vars' = fold Term.add_term_varnames vs vars;
    9.84 @@ -2242,7 +2242,7 @@
    9.85      val renameT =
    9.86            if is_local then I
    9.87            else Type.unvarifyT o Term.map_type_tfree (fn (a, s) =>
    9.88 -            TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
    9.89 +            TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
    9.90      val rename =
    9.91            if is_local then I
    9.92            else Term.map_term_types renameT;
    9.93 @@ -2269,7 +2269,7 @@
    9.94  
    9.95      (* restore "small" ids *)
    9.96      val ids' = map (fn ((n, ps), (_, mode)) =>
    9.97 -          ((n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps), mode)) ids;
    9.98 +          ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids;
    9.99      (* instantiate ids and elements *)
   9.100      val inst_elemss = map
   9.101            (fn ((id, _), ((_, mode), elems)) =>
   9.102 @@ -2348,8 +2348,8 @@
   9.103          fun activate_reg (vts, ((prfx, atts2), _)) thy = let
   9.104              val ((inst, tinst), wits) =
   9.105                  collect_global_witnesses thy fixed t_ids vts;
   9.106 -            fun inst_parms ps = map (fn p =>
   9.107 -                  valOf (assoc (map #1 fixed ~~ vts, p))) ps;
   9.108 +            fun inst_parms ps = map 
   9.109 +                  (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
   9.110              val disch = Drule.fconv_rule (Thm.beta_conversion true) o
   9.111                  Drule.satisfy_hyps wits;
   9.112              val new_elemss = List.filter (fn (((name, ps), _), _) =>