# HG changeset patch
# User wenzelm
# Date 1486655907 -3600
# Node ID 14641ca387f8c622d83a285346e316abcbbc4d73
# Parent  42bffd1637f016d14631b1899b1d184c5ccfdd01
tuned;

diff -r 42bffd1637f0 -r 14641ca387f8 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Feb 09 16:56:31 2017 +0100
+++ b/src/Pure/General/sql.scala	Thu Feb 09 16:58:27 2017 +0100
@@ -195,6 +195,9 @@
   }
 
 
+
+  /** SQL database operations **/
+
   /* results */
 
   def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
@@ -204,10 +207,6 @@
     def next: A = { val x = get(rs); _next = rs.next(); x }
   }
 
-
-
-  /** SQL database operations **/
-
   trait Database
   {
     /* types */