# HG changeset patch
# User wenzelm
# Date 1494063823 -7200
# Node ID 3f206cfca625883bcc93166ec270422d2f1be67d
# Parent  6bfe25513851835cb3e67a64db5c60814a83fccf
unused;

diff -r 6bfe25513851 -r 3f206cfca625 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat May 06 11:43:35 2017 +0200
+++ b/src/Pure/General/sql.scala	Sat May 06 11:43:43 2017 +0200
@@ -45,13 +45,6 @@
   def select(columns: List[Column], distinct: Boolean = false): Source =
     "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.ident)) + " FROM "
 
-  def join(table1: Table, table2: Table, sql: Source = "", outer: Boolean = false): Source =
-    table1 + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2 +
-      (if (sql == "") "" else " ON " + sql)
-
-  def join_outer(table1: Table, table2: Table, sql: Source = ""): Source =
-    join(table1, table2, sql, outer = true)
-
 
   /* types */