# HG changeset patch
# User paulson
# Date 875183129 -7200
# Node ID 8a1f7d5b1eff9e4d0b08603d634d98365313072e
# Parent  242546f35f8ed0e75550cde1b06efdf6bbe073cc
Deleted the unused list_mk_disj

diff -r 242546f35f8e -r 8a1f7d5b1eff TFL/usyntax.sig
--- 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)
diff -r 242546f35f8e -r 8a1f7d5b1eff TFL/usyntax.sml
--- 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? *)