src/ZF/Tools/inductive_package.ML

   val dummy = assert_all is_Free rec_params
       (fn t => "Param in recursion term not a free variable: " ^
                Syntax.string_of_term ctxt t);
 
   (*** Construct the fixedpoint definition ***)
-  val mk_variant = Name.variant (foldr OldTerm.add_term_names [] intr_tms);
+  val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
   fun dest_tprop (Const("Trueprop",_) $ P) = P
     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^

   fun fp_part intr = (*quantify over rule's free vars except parameters*)
     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
         val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
         val exfrees = OldTerm.term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
-    in foldr FOLogic.mk_exists
+    in List.foldr FOLogic.mk_exists
              (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
   fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)

        | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
 
      (*Make a premise of the induction rule.*)
      fun induct_prem ind_alist intr =
        let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
-           val iprems = foldr (add_induct_prem ind_alist) []
+           val iprems = List.foldr (add_induct_prem ind_alist) []
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr
            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

      fun mk_predpair rec_tm =
        let val rec_name = (#1 o dest_Const o head_of) rec_tm
            val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
                             elem_factors ---> FOLogic.oT)
            val qconcl =
-             foldr FOLogic.mk_all
+             List.foldr FOLogic.mk_all
                (FOLogic.imp $
                 (@{const mem} $ elem_tuple $ rec_tm)
                       $ (list_comb (pfree, elem_frees))) elem_frees
        in  (CP.ap_split elem_type FOLogic.oT pfree,
             qconcl)