TFL/usyntax.ML
changeset 16853 33b886cbdc8f
parent 15531 08c8dad8e399
child 18176 ae9bd644d106
     1.1 --- a/TFL/usyntax.ML	Thu Jul 14 19:28:37 2005 +0200
     1.2 +++ b/TFL/usyntax.ML	Thu Jul 14 19:28:38 2005 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  val is_vartype = can dest_vtype;
     1.5  
     1.6  val type_vars  = map mk_prim_vartype o typ_tvars
     1.7 -fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
     1.8 +fun type_varsl L = distinct (fold (curry op @ o type_vars) L []);
     1.9  
    1.10  val alpha  = mk_vartype "'a"
    1.11  val beta   = mk_vartype "'b"
    1.12 @@ -312,11 +312,11 @@
    1.13  
    1.14  (* Construction of a cterm from a list of Terms *)
    1.15  
    1.16 -fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
    1.17 +fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
    1.18  
    1.19  (* These others are almost never used *)
    1.20 -fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
    1.21 -fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
    1.22 +fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
    1.23 +fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
    1.24  val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
    1.25  
    1.26