--- a/TFL/usyntax.sig Thu Sep 25 12:24:53 1997 +0200
+++ b/TFL/usyntax.sig Thu Sep 25 12:25:29 1997 +0200
@@ -76,7 +76,6 @@
val list_mk_imp : (term list * term) -> term
val list_mk_forall : (term list * term) -> term
val list_mk_conj : term list -> term
- val list_mk_disj : term list -> term
(* Destructing a term to a list of Preterms *)
val strip_comb : term -> (term * term list)
--- a/TFL/usyntax.sml Thu Sep 25 12:24:53 1997 +0200
+++ b/TFL/usyntax.sml Thu Sep 25 12:25:29 1997 +0200
@@ -239,7 +239,6 @@
fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
-val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
(* Need to reverse? *)