src/ZF/Tools/inductive_package.ML

      (*Used to make induction rules;
         ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
         prem is a premise of an intr rule*)
      fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
                       (Const("op :",_)$t$X), iprems) =
-          (case gen_assoc (op aconv) (ind_alist, X) of
+          (case AList.lookup (op aconv) ind_alist X of
                SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
                  let fun mk_sb (rec_tm,pred) =
                              (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
                  in  subst_free (map mk_sb ind_alist) prem :: iprems  end)

      fun induct_prem ind_alist intr =
        let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
            val iprems = foldr (add_induct_prem ind_alist) []
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr
-           val (SOME pred) = gen_assoc (op aconv) (ind_alist, X)
+           val (SOME pred) = AList.lookup (op aconv) ind_alist X
            val concl = FOLogic.mk_Trueprop (pred $ t)
        in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
        handle Bind => error"Recursion term not found in conclusion";
 
      (*Minimizes backtracking by delivering the correct premise to each goal.