# HG changeset patch
# User wenzelm
# Date 1121362118 -7200
# Node ID 33b886cbdc8fe2db59ee3079245a2cfa8ad6257e
# Parent  b950180e243d1d9b160971e4cb96fce6e77a8380
replaced itlist by fold_rev;
replaced rev_itlist by fold;

diff -r b950180e243d -r 33b886cbdc8f TFL/rules.ML
--- a/TFL/rules.ML	Thu Jul 14 19:28:37 2005 +0200
+++ b/TFL/rules.ML	Thu Jul 14 19:28:38 2005 +0200
@@ -128,7 +128,7 @@
 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 =
@@ -202,9 +202,9 @@
         | 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;
 
 
@@ -287,10 +287,10 @@
    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
@@ -318,7 +318,7 @@
    end
 end;
 
-val GENL = U.itlist GEN;
+val GENL = fold_rev GEN;
 
 fun GEN_ALL thm =
    let val {prop,sign,...} = rep_thm thm
@@ -383,7 +383,7 @@
  *---------------------------------------------------------------------------*)
 
 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;
 
 
@@ -404,7 +404,7 @@
        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)
@@ -527,7 +527,7 @@
       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;
 
 
@@ -567,7 +567,7 @@
   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
@@ -765,7 +765,7 @@
                    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
diff -r b950180e243d -r 33b886cbdc8f TFL/tfl.ML
--- a/TFL/tfl.ML	Thu Jul 14 19:28:37 2005 +0200
+++ b/TFL/tfl.ML	Thu Jul 14 19:28:38 2005 +0200
@@ -104,7 +104,7 @@
           let val (c, T) = dest_Const c
               val L = binder_types T
               val (in_group, not_in_group) =
-               U.itlist (fn (row as (p::rst, rhs)) =>
+               fold_rev (fn (row as (p::rst, rhs)) =>
                          fn (in_group,not_in_group) =>
                   let val (pc,args) = S.strip_comb p
                   in if (#1(dest_Const pc) = c)
@@ -160,7 +160,7 @@
  * pattern with constructor = name.
  *---------------------------------------------------------------------------*)
 fun mk_group name rows =
-  U.itlist (fn (row as ((prfx, p::rst), rhs)) =>
+  fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
             fn (in_group,not_in_group) =>
                let val (pc,args) = S.strip_comb p
                in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
@@ -565,14 +565,14 @@
      val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
          (*lcp: a lot of object-logic inference to remove*)
      val baz = R.DISCH_ALL
-                 (U.itlist R.DISCH full_rqt_prop
+                 (fold_rev R.DISCH full_rqt_prop
                   (R.LIST_CONJ extractants))
      val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
                            else ()
      val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
      val SV' = map tych SV;
      val SVrefls = map reflexive SV'
-     val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x))
+     val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
                    SVrefls def)
                 RS meta_eq_to_obj_eq
      val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
@@ -584,7 +584,7 @@
     "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
      val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
  in {theory = theory, R=R1, SV=SV,
-     rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
+     rules = fold (U.C R.MP) (R.CONJUNCTS bar) def',
      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
      patterns = pats}
  end;
@@ -834,7 +834,7 @@
       val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
       val {lhs,rhs} = S.dest_eq veq
       val L = S.free_vars_lr rhs
-  in  #2 (U.itlist CHOOSER L (veq,thm))  end;
+  in  #2 (fold_rev CHOOSER L (veq,thm))  end;
 
 
 (*----------------------------------------------------------------------------
@@ -873,7 +873,7 @@
     val dc = R.MP Sinduct dant
     val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
     val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
-    val dc' = U.itlist (R.GEN o tych) vars
+    val dc' = fold_rev (R.GEN o tych) vars
                        (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
 in
    R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
@@ -999,7 +999,7 @@
         let val tcs = #1(strip_imp (concl r))
             val extra_tcs = gen_rems (op aconv) (ftcs, tcs)
             val extra_tc_thms = map simplify_nested_tc extra_tcs
-            val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind)
+            val (r1,ind1) = fold simplify_tc tcs (r,ind)
             val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
         in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
         end
diff -r b950180e243d -r 33b886cbdc8f TFL/usyntax.ML
--- a/TFL/usyntax.ML	Thu Jul 14 19:28:37 2005 +0200
+++ b/TFL/usyntax.ML	Thu Jul 14 19:28:38 2005 +0200
@@ -115,7 +115,7 @@
 val is_vartype = can dest_vtype;
 
 val type_vars  = map mk_prim_vartype o typ_tvars
-fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
+fun type_varsl L = distinct (fold (curry op @ o type_vars) L []);
 
 val alpha  = mk_vartype "'a"
 val beta   = mk_vartype "'b"
@@ -312,11 +312,11 @@
 
 (* Construction of a cterm from a list of Terms *)
 
-fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
+fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
 
 (* These others are almost never used *)
-fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
-fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
+fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
+fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
 val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})