diff -r a0ed7bc688b5 -r 70072780e095 src/Pure/term.scala
--- a/src/Pure/term.scala	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/term.scala	Sun Jul 10 20:59:04 2011 +0200
@@ -31,58 +31,61 @@
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
+}
+
+
+object Term_XML
+{
+  import Term._
 
 
   /* XML data representation */
 
-  object XML
+  object Encode
   {
-    object Make
-    {
-      import XML_Data.Make._
+    import XML_Data.Encode._
 
-      val indexname: T[Indexname] = pair(string, int)
+    val indexname: T[Indexname] = pair(string, int)
 
-      val sort: T[Sort] = list(string)
+    val sort: T[Sort] = list(string)
 
-      def typ: T[Typ] =
-        variant[Typ](List(
-          { case Type(a, b) => pair(string, list(typ))((a, b)) },
-          { case TFree(a, b) => pair(string, sort)((a, b)) },
-          { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
+    def typ: T[Typ] =
+      variant[Typ](List(
+        { case Type(a, b) => pair(string, list(typ))((a, b)) },
+        { case TFree(a, b) => pair(string, sort)((a, b)) },
+        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
 
-      def term: T[Term] =
-        variant[Term](List(
-          { case Const(a, b) => pair(string, typ)((a, b)) },
-          { case Free(a, b) => pair(string, typ)((a, b)) },
-          { case Var(a, b) => pair(indexname, typ)((a, b)) },
-          { case Bound(a) => int(a) },
-          { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
-          { case App(a, b) => pair(term, term)((a, b)) }))
-    }
+    def term: T[Term] =
+      variant[Term](List(
+        { case Const(a, b) => pair(string, typ)((a, b)) },
+        { case Free(a, b) => pair(string, typ)((a, b)) },
+        { case Var(a, b) => pair(indexname, typ)((a, b)) },
+        { case Bound(a) => int(a) },
+        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
+        { case App(a, b) => pair(term, term)((a, b)) }))
+  }
 
-    object Dest
-    {
-      import XML_Data.Dest._
+  object Decode
+  {
+    import XML_Data.Decode._
 
-      val indexname: T[Indexname] = pair(string, int)
+    val indexname: T[Indexname] = pair(string, int)
 
-      val sort: T[Sort] = list(string)
+    val sort: T[Sort] = list(string)
 
-      def typ: T[Typ] =
-        variant[Typ](List(
-          (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
-          (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
-          (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
+    def typ: T[Typ] =
+      variant[Typ](List(
+        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
+        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
+        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
 
-      def term: T[Term] =
-        variant[Term](List(
-          (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
-          (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
-          (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
-          (x => Bound(int(x))),
-          (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
-          (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
-    }
+    def term: T[Term] =
+      variant[Term](List(
+        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
+        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
+        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
+        (x => Bound(int(x))),
+        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
+        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
   }
 }