# HG changeset patch
# User wenzelm
# Date 1219504973 -7200
# Node ID 0576c91a68034ad7f47657ea566da6be1786aae3
# Parent  8adddc0b591f60ed1cc39f59a9032080071345a7
tuned;

diff -r 8adddc0b591f -r 0576c91a6803 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Sat Aug 23 17:22:52 2008 +0200
+++ b/src/Pure/General/xml.scala	Sat Aug 23 17:22:53 2008 +0200
@@ -59,18 +59,18 @@
     }
 
     // main body
-    def dom_tree(tr: Tree): Node = tr match {
+    def DOM(tr: Tree): Node = tr match {
       case Elem(name, atts, ts) => {
         val node = doc.createElement(name)
         for ((name, value) <- atts) node.setAttribute(name, value)
-        for (t <- ts) node.appendChild(dom_tree(t))
+        for (t <- ts) node.appendChild(DOM(t))
         node
       }
       case Text(txt) => doc.createTextNode(txt)
     }
     val root_elem = tree match {
-      case Elem(_, _, _) => dom_tree(tree)
-      case Text(_) => dom_tree(Elem("root", Nil, List(tree)))
+      case Elem(_, _, _) => DOM(tree)
+      case Text(_) => DOM(Elem("root", Nil, List(tree)))
     }
     doc.appendChild(root_elem)
     doc