more abstract signature;
tuned;

--- a/src/Pure/General/xml_data.ML	Sun Jul 10 13:51:21 2011 +0200
+++ b/src/Pure/General/xml_data.ML	Sun Jul 10 15:48:15 2011 +0200
@@ -8,31 +8,33 @@
 sig
   structure Make:
   sig
-    val properties: Properties.T -> XML.body
-    val string: string -> XML.body
-    val int: int -> XML.body
-    val bool: bool -> XML.body
-    val unit: unit -> XML.body
-    val pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
-    val triple: ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
-    val list: ('a -> XML.body) -> 'a list -> XML.body
-    val option: ('a -> XML.body) -> 'a option -> XML.body
-    val variant: ('a -> XML.body) list -> 'a -> XML.body
+    type 'a T = 'a -> XML.body
+    val properties: Properties.T T
+    val string: string T
+    val int: int T
+    val bool: bool T
+    val unit: unit T
+    val pair: 'a T -> 'b T -> ('a * 'b) T
+    val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
+    val list: 'a T -> 'a list T
+    val option: 'a T -> 'a option T
+    val variant: 'a T list -> 'a T
   end
   exception XML_ATOM of string
   exception XML_BODY of XML.body
   structure Dest:
   sig
-    val properties: XML.body -> Properties.T
-    val string : XML.body -> string
-    val int : XML.body -> int
-    val bool: XML.body -> bool
-    val unit: XML.body -> unit
-    val pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
-    val triple: (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
-    val list: (XML.body -> 'a) -> XML.body -> 'a list
-    val option: (XML.body -> 'a) -> XML.body -> 'a option
-    val variant: (XML.body -> 'a) list -> XML.body -> 'a
+    type 'a T = XML.body -> 'a
+    val properties: Properties.T T
+    val string : string T
+    val int : int T
+    val bool: bool T
+    val unit: unit T
+    val pair: 'a T -> 'b T -> ('a * 'b) T
+    val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
+    val list: 'a T -> 'a list T
+    val option: 'a T -> 'a option T
+    val variant: 'a T list -> 'a T
   end
 end;
 
@@ -44,6 +46,9 @@
 structure Make =
 struct
 
+type 'a T = 'a -> XML.body;
+
+
 (* basic values *)
 
 fun int_atom i = signed_string_of_int i;
@@ -97,6 +102,9 @@
 structure Dest =
 struct
 
+type 'a T = XML.body -> 'a;
+
+
 (* basic values *)
 
 fun int_atom s =

--- a/src/Pure/General/xml_data.scala	Sun Jul 10 13:51:21 2011 +0200
+++ b/src/Pure/General/xml_data.scala	Sun Jul 10 15:48:15 2011 +0200
@@ -14,6 +14,9 @@
 
   object Make
   {
+    type T[A] = A => XML.Body
+
+
     /* basic values */
 
     private def long_atom(i: Long): String = i.toString
@@ -35,39 +38,39 @@
 
     /* representation of standard types */
 
-    def properties(props: List[(String, String)]): XML.Body =
-      List(XML.Elem(Markup(":", props), Nil))
+    val properties: T[List[(String, String)]] =
+      (props => List(XML.Elem(Markup(":", props), Nil)))
 
-    def string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
+    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
 
-    def long(i: Long): XML.Body = string(long_atom(i))
+    val long: T[Long] = (x => string(long_atom(x)))
 
-    def int(i: Int): XML.Body = string(int_atom(i))
+    val int: T[Int] = (x => string(int_atom(x)))
 
-    def bool(b: Boolean): XML.Body = string(bool_atom(b))
+    val bool: T[Boolean] = (x => string(bool_atom(x)))
 
-    def unit(u: Unit): XML.Body = string(unit_atom(u))
+    val unit: T[Unit] = (x => string(unit_atom(x)))
 
-    def pair[A, B](f: A => XML.Body, g: B => XML.Body)(p: (A, B)): XML.Body =
-      List(node(f(p._1)), node(g(p._2)))
+    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+      (x => List(node(f(x._1)), node(g(x._2))))
 
-    def triple[A, B, C](f: A => XML.Body, g: B => XML.Body, h: C => XML.Body)
-        (p: (A, B, C)): XML.Body =
-      List(node(f(p._1)), node(g(p._2)), node(h(p._3)))
+    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
 
-    def list[A](f: A => XML.Body)(xs: List[A]): XML.Body =
-      xs.map((x: A) => node(f(x)))
+    def list[A](f: T[A]): T[List[A]] =
+      (xs => xs.map((x: A) => node(f(x))))
 
-    def option[A](f: A => XML.Body)(opt: Option[A]): XML.Body =
-      opt match {
-        case None => Nil
-        case Some(x) => List(node(f(x)))
-      }
+    def option[A](f: T[A]): T[Option[A]] =
+    {
+      case None => Nil
+      case Some(x) => List(node(f(x)))
+    }
 
-    def variant[A](fs: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
+    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
     {
-      val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
-      List(tagged(tag, f(x)))
+      case x =>
+        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+        List(tagged(tag, f(x)))
     }
   }
 
@@ -80,6 +83,9 @@
 
   object Dest
   {
+    type T[A] = XML.Body => A
+
+
      /* basic values */
 
     private def long_atom(s: String): Long =
@@ -116,56 +122,55 @@
 
     /* representation of standard types */
 
-    def properties(ts: XML.Body): List[(String, String)] =
-      ts match {
-        case List(XML.Elem(Markup(":", props), Nil)) => props
-        case _ => throw new XML_Body(ts)
-      }
+    val properties: T[List[(String, String)]] =
+    {
+      case List(XML.Elem(Markup(":", props), Nil)) => props
+      case ts => throw new XML_Body(ts)
+    }
 
-    def string(ts: XML.Body): String =
-      ts match {
-        case Nil => ""
-        case List(XML.Text(s)) => s
-        case _ => throw new XML_Body(ts)
-      }
+    val string: T[String] =
+    {
+      case Nil => ""
+      case List(XML.Text(s)) => s
+      case ts => throw new XML_Body(ts)
+    }
 
-    def long(ts: XML.Body): Long = long_atom(string(ts))
+    val long: T[Long] = (x => long_atom(string(x)))
 
-    def int(ts: XML.Body): Int = int_atom(string(ts))
+    val int: T[Int] = (x => int_atom(string(x)))
 
-    def bool(ts: XML.Body) = bool_atom(string(ts))
+    val bool: T[Boolean] = (x => bool_atom(string(x)))
 
-    def unit(ts: XML.Body): Unit = unit_atom(string(ts))
+    val unit: T[Unit] = (x => unit_atom(string(x)))
 
-    def pair[A, B](f: XML.Body => A, g: XML.Body => B)(ts: XML.Body): (A, B) =
-      ts match {
-        case List(t1, t2) => (f(node(t1)), g(node(t2)))
-        case _ => throw new XML_Body(ts)
-      }
+    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+    {
+      case List(t1, t2) => (f(node(t1)), g(node(t2)))
+      case ts => throw new XML_Body(ts)
+    }
 
-    def triple[A, B, C](f: XML.Body => A, g: XML.Body => B, h: XML.Body => C)
-        (ts: XML.Body): (A, B, C) =
-      ts match {
-        case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
-        case _ => throw new XML_Body(ts)
-      }
+    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+    {
+      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
+      case ts => throw new XML_Body(ts)
+    }
+
+    def list[A](f: T[A]): T[List[A]] =
+      (ts => ts.map(t => f(node(t))))
 
-    def list[A](f: XML.Body => A)(ts: XML.Body): List[A] =
-      ts.map((t: XML.Tree) => f(node(t)))
+    def option[A](f: T[A]): T[Option[A]] =
+    {
+      case Nil => None
+      case List(t) => Some(f(node(t)))
+      case ts => throw new XML_Body(ts)
+    }
 
-    def option[A](f: XML.Body => A)(ts: XML.Body): Option[A] =
-      ts match {
-        case Nil => None
-        case List(t) => Some(f(node(t)))
-        case _ => throw new XML_Body(ts)
-      }
-
-    def variant[A](fs: List[XML.Body => A])(ts: XML.Body): A =
-      ts match {
-        case List(t) =>
-          val (tag, ts) = tagged(t)
-          fs(tag)(ts)
-        case _ => throw new XML_Body(ts)
-      }
+    def variant[A](fs: List[T[A]]): T[A] =
+    {
+      case List(t) =>
+        val (tag, ts) = tagged(t)
+        fs(tag)(ts)
+      case ts => throw new XML_Body(ts)
+    }
   }
 }

--- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:51:21 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 15:48:15 2011 +0200
@@ -31,9 +31,12 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
-  def make_xml_data(header: Header): XML.Body =
-  { import XML_Data.Make._
-    triple(string, list(string), list(string))(header.name, header.imports, header.uses) }
+  val make_xml_data: XML_Data.Make.T[Header] =
+  {
+    case Header(name, imports, uses) =>
+      import XML_Data.Make._
+      triple(string, list(string), list(string))(name, imports, uses)
+  }
 
 
   /* file name */