--- a/src/HOL/Tools/datatype_realizer.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Sep 20 16:17:34 2005 +0200
@@ -141,7 +141,7 @@
val rvs = Drule.vars_of_terms [prop_of thm'];
val ivs1 = map Var (filter_out (fn (_, T) =>
tname_of (body_type T) mem ["set", "bool"]) ivs);
- val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
+ val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
val prf = foldr forall_intr_prf
(foldr (fn ((f, p), prf) =>
@@ -182,7 +182,7 @@
list_comb (r, free_ts)))))
end;
- val SOME (_, _, constrs) = assoc (descr, index);
+ val SOME (_, _, constrs) = AList.lookup (op =) descr index;
val T = List.nth (get_rec_types descr sorts, index);
val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
val r = Const (case_name, map fastype_of rs ---> T --> rT);