src/ZF/Tools/inductive_package.ML

   val dummy = assert_all is_Free rec_params
       (fn t => "Param in recursion term not a free variable: " ^
                Sign.string_of_term sign t);
 
   (*** Construct the fixedpoint definition ***)
-  val mk_variant = variant (foldr add_term_names (intr_tms, []));
+  val mk_variant = variant (Library.foldr 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: " ^
                             Sign.string_of_term sign Q);
 
   (*Makes a disjunct from an introduction rule*)
   fun fp_part intr = (*quantify over rule's free vars except parameters*)
     let val prems = map dest_tprop (strip_imp_prems intr)
-        val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
+        val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
         val exfrees = term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
-    in foldr FOLogic.mk_exists
+    in Library.foldr FOLogic.mk_exists
              (exfrees, fold_bal FOLogic.mk_conj (zeq::prems))
     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*)

                    mk_Collect(z', dom_sum,
                               fold_bal FOLogic.mk_disj part_intrs));
 
   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
 
-  val dummy = seq (fn rec_hd => deny (rec_hd occs fp_rhs)
+  val dummy = List.app (fn rec_hd => deny (rec_hd occs fp_rhs)
                              "Illegal occurrence of recursion operator")
            rec_hds;
 
   (*** Make the new theory ***)
 

            | _ => rec_tms ~~          (*define the sets as Parts*)
                   map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
 
   (*tracing: print the fixedpoint definition*)
   val dummy = if !Ind_Syntax.trace then
-              seq (writeln o Sign.string_of_term sign o #2) axpairs
+              List.app (writeln o Sign.string_of_term sign o #2) axpairs
           else ()
 
   (*add definitions of the inductive sets*)
   val thy1 = thy |> Theory.add_path big_rec_base_name
                  |> (#1 o PureThy.add_defs_i false (map Thm.no_attributes axpairs))

        | 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 (term_frees intr \\ rec_params)
-           val iprems = foldr (add_induct_prem ind_alist)
+           val iprems = Library.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 concl = FOLogic.mk_Trueprop (pred $ t)
        in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end

      val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
                          intr_tms;
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln "ind_prems = ";
-                  seq (writeln o Sign.string_of_term sign1) ind_prems;
+                  List.app (writeln o Sign.string_of_term sign1) ind_prems;
                   writeln "raw_induct = "; print_thm raw_induct)
              else ();
 
 
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.

      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
+             Library.foldr FOLogic.mk_all
                (elem_frees,
                 FOLogic.imp $
                 (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
                       $ (list_comb (pfree, elem_frees)))
        in  (CP.ap_split elem_type FOLogic.oT pfree,