--- a/TFL/dcterm.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/dcterm.sml Thu Jun 05 13:27:28 1997 +0200
@@ -35,8 +35,6 @@
val is_let : cterm -> bool
val is_neg : cterm -> bool
val is_pair : cterm -> bool
- val list_mk_abs : cterm list -> cterm -> cterm
- val list_mk_exists : cterm list * cterm -> cterm
val list_mk_disj : cterm list -> cterm
val strip_abs : cterm -> cterm list * cterm
val strip_comb : cterm -> cterm * cterm list
@@ -57,14 +55,6 @@
val can = Utils.can;
fun swap (x,y) = (y,x);
-fun itlist f L base_value =
- let fun it [] = base_value
- | it (a::rst) = f a (it rst)
- in it L
- end;
-
-val end_itlist = Utils.end_itlist;
-
(*---------------------------------------------------------------------------
* Some simple constructor functions.
@@ -164,10 +154,7 @@
(*---------------------------------------------------------------------------
* Iterated creation.
*---------------------------------------------------------------------------*)
-val list_mk_abs = itlist cabs;
-
-fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
-val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
+val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
(*---------------------------------------------------------------------------
* Iterated destruction. (To the "right" in a term.)