TFL/rules.ML

 
 (*forces the first argument to be a proposition if necessary*)
 fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
   handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
 
-fun DISCH_ALL thm = U.itlist DISCH (#hyps (Thm.crep_thm thm)) thm;
+fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
 
 
 fun FILTER_DISCH_ALL P thm =
  let fun check tm = P (#t (Thm.rep_cterm tm))
  in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)

 fun EVEN_ORS thms =
   let fun blue ldisjs [] _ = []
         | blue ldisjs (th::rst) rdisjs =
             let val tail = tl rdisjs
                 val rdisj_tl = D.list_mk_disj tail
-            in U.itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
+            in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
                :: blue (ldisjs @ [cconcl th]) rst tail
-            end handle U.ERR _ => [U.itlist DISJ2 ldisjs th]
+            end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
    in blue [] thms (map cconcl thms) end;
 
 
 (*----------------------------------------------------------------------------
  *

    in
       thm RS (forall_elim tm gspec')
    end
 end;
 
-fun SPEC_ALL thm = U.rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
+fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
 
 val ISPEC = SPEC
-val ISPECL = U.rev_itlist ISPEC;
+val ISPECL = fold ISPEC;
 
 (* Not optimized! Too complicated. *)
 local val {prop,sign,...} = rep_thm allI
       val [P] = add_term_vars (prop, [])
       fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))

        val prop' = tp $ (A $ Abs(x,ty,M))
    in ALPHA thm (cterm_of sign prop')
    end
 end;
 
-val GENL = U.itlist GEN;
+val GENL = fold_rev GEN;
 
 fun GEN_ALL thm =
    let val {prop,sign,...} = rep_thm thm
        val tycheck = cterm_of sign
        val vlist = map tycheck (add_term_vars (prop, []))

  *    A |- ?v1...v_n. M
  *
  *---------------------------------------------------------------------------*)
 
 fun EXISTL vlist th =
-  U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
+  fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
            vlist th;
 
 
 (*----------------------------------------------------------------------------
  *

        val detype = #t o rep_cterm
        val blist' = map (fn (x,y) => (detype x, detype y)) blist
        fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
 
   in
-  U.itlist (fn (b as (r1,r2)) => fn thm =>
+  fold_rev (fn (b as (r1,r2)) => fn thm =>
         EXISTS(?r2(subst_free[b]
                    (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
               thm)
        blist' th
   end;

   let val {prop,sign,...} = rep_thm thm
       val tych = cterm_of sign
       val ants = Logic.strip_imp_prems prop
       val news = get (ants,1,[])
   in
-  U.rev_itlist rename_params_rule news thm
+  fold rename_params_rule news thm
   end;
 
 
 (*---------------------------------------------------------------------------
  * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)

 fun mk_aabs (vstr, body) =
   S.mk_abs {Bvar = vstr, Body = body}
   handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
 
 fun list_mk_aabs (vstrl,tm) =
-    U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
+    fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
 
 fun dest_aabs used tm =
    let val ({Bvar,Body}, used') = S.dest_abs used tm
    in (Bvar, Body, used') end
    handle U.ERR _ =>

               val dummy = print_thms "cntxt:" cntxt
               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                    sign,...} = rep_thm thm
               fun genl tm = let val vlist = gen_rems (op aconv)
                                            (add_term_frees(tm,[]), globals)
-                            in U.itlist Forall vlist tm
+                            in fold_rev Forall vlist tm
                             end
               (*--------------------------------------------------------------
                * This actually isn't quite right, since it will think that
                * not-fully applied occs. of "f" in the context mean that the
                * current call is nested. The real solution is to pass in a