src/HOL/Tools/datatype_realizer.ML
changeset 17521 0f1c48de39f5
parent 16123 1381e90c2694
child 17959 8db36a108213
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -141,7 +141,7 @@
     1.4      val rvs = Drule.vars_of_terms [prop_of thm'];
     1.5      val ivs1 = map Var (filter_out (fn (_, T) =>
     1.6        tname_of (body_type T) mem ["set", "bool"]) ivs);
     1.7 -    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
     1.8 +    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
     1.9  
    1.10      val prf = foldr forall_intr_prf
    1.11       (foldr (fn ((f, p), prf) =>
    1.12 @@ -182,7 +182,7 @@
    1.13              list_comb (r, free_ts)))))
    1.14        end;
    1.15  
    1.16 -    val SOME (_, _, constrs) = assoc (descr, index);
    1.17 +    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
    1.18      val T = List.nth (get_rec_types descr sorts, index);
    1.19      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    1.20      val r = Const (case_name, map fastype_of rs ---> T --> rT);