# HG changeset patch
# User wenzelm
# Date 1310298681 -7200
# Node ID 4e58485fa320c9a5b6afe58f48f2bbf44c471543
# Parent  8a63c95b1d5bbf03d33a5b53c04e0e6de2c14388
simplified XML_Data;

diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/General/xml_data.ML
--- a/src/Pure/General/xml_data.ML	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/General/xml_data.ML	Sun Jul 10 13:51:21 2011 +0200
@@ -6,137 +6,152 @@
 
 signature XML_DATA =
 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
+  end
   exception XML_ATOM of string
   exception XML_BODY of XML.body
-  val make_properties: Properties.T -> XML.body
-  val dest_properties: XML.body -> Properties.T
-  val make_string: string -> XML.body
-  val dest_string : XML.body -> string
-  val make_int: int -> XML.body
-  val dest_int : XML.body -> int
-  val make_bool: bool -> XML.body
-  val dest_bool: XML.body -> bool
-  val make_unit: unit -> XML.body
-  val dest_unit: XML.body -> unit
-  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
-  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
-  val make_triple:
-    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
-  val dest_triple:
-    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
-  val make_list: ('a -> XML.body) -> 'a list -> XML.body
-  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
-  val make_option: ('a -> XML.body) -> 'a option -> XML.body
-  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
-  val make_variant: ('a -> XML.body) list -> 'a -> XML.body
-  val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a
+  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
+  end
 end;
 
 structure XML_Data: XML_DATA =
 struct
 
+(** make **)
+
+structure Make =
+struct
+
 (* basic values *)
 
-exception XML_ATOM of string;
-
-
-fun make_int_atom i = signed_string_of_int i;
-
-fun dest_int_atom s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise XML_ATOM s);
-
+fun int_atom i = signed_string_of_int i;
 
-fun make_bool_atom false = "0"
-  | make_bool_atom true = "1";
+fun bool_atom false = "0"
+  | bool_atom true = "1";
 
-fun dest_bool_atom "0" = false
-  | dest_bool_atom "1" = true
-  | dest_bool_atom s = raise XML_ATOM s;
-
-
-fun make_unit_atom () = "";
-
-fun dest_unit_atom "" = ()
-  | dest_unit_atom s = raise XML_ATOM s;
+fun unit_atom () = "";
 
 
 (* structural nodes *)
 
-exception XML_BODY of XML.tree list;
-
-fun make_node ts = XML.Elem ((":", []), ts);
+fun node ts = XML.Elem ((":", []), ts);
 
-fun dest_node (XML.Elem ((":", []), ts)) = ts
-  | dest_node t = raise XML_BODY [t];
-
-fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts);
-
-fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts)
-  | dest_tagged t = raise XML_BODY [t];
+fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
 
 
 (* representation of standard types *)
 
-fun make_properties props = [XML.Elem ((":", props), [])];
-
-fun dest_properties [XML.Elem ((":", props), [])] = props
-  | dest_properties ts = raise XML_BODY ts;
-
+fun properties props = [XML.Elem ((":", props), [])];
 
-fun make_string "" = []
-  | make_string s = [XML.Text s];
-
-fun dest_string [] = ""
-  | dest_string [XML.Text s] = s
-  | dest_string ts = raise XML_BODY ts;
-
+fun string "" = []
+  | string s = [XML.Text s];
 
-val make_int = make_string o make_int_atom;
-val dest_int = dest_int_atom o dest_string;
-
-val make_bool = make_string o make_bool_atom;
-val dest_bool = dest_bool_atom o dest_string;
+val int = string o int_atom;
 
-val make_unit = make_string o make_unit_atom;
-val dest_unit = dest_unit_atom o dest_string;
-
+val bool = string o bool_atom;
 
-fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
-
-fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
-  | dest_pair _ _ ts = raise XML_BODY ts;
+val unit = string o unit_atom;
 
-
-fun make_triple make1 make2 make3 (x, y, z) =
-  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
+fun pair f g (x, y) = [node (f x), node (g y)];
 
-fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
-      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
-  | dest_triple _ _ _ ts = raise XML_BODY ts;
-
-
-fun make_list make xs = map (make_node o make) xs;
-
-fun dest_list dest ts = map (dest o dest_node) ts;
-
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
 
-fun make_option _ NONE = []
-  | make_option make (SOME x) = [make_node (make x)];
-
-fun dest_option _ [] = NONE
-  | dest_option dest [t] = SOME (dest (dest_node t))
-  | dest_option _ ts = raise XML_BODY ts;
-
+fun list f xs = map (node o f) xs;
 
-fun make_variant makes x =
-  [make_tagged (the (get_index (fn make => try make x) makes))];
+fun option _ NONE = []
+  | option f (SOME x) = [node (f x)];
 
-fun dest_variant dests [t] =
-      let val (tag, ts) = dest_tagged t
-      in nth dests tag ts end
-  | dest_variant _ ts = raise XML_BODY ts;
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
 
 end;
 
+
+
+(** dest **)
+
+exception XML_ATOM of string;
+exception XML_BODY of XML.tree list;
+
+structure Dest =
+struct
+
+(* basic values *)
+
+fun int_atom s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => raise XML_ATOM s);
+
+fun bool_atom "0" = false
+  | bool_atom "1" = true
+  | bool_atom s = raise XML_ATOM s;
+
+fun unit_atom "" = ()
+  | unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+fun node (XML.Elem ((":", []), ts)) = ts
+  | node t = raise XML_BODY [t];
+
+fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
+  | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun properties [XML.Elem ((":", props), [])] = props
+  | properties ts = raise XML_BODY ts;
+
+fun string [] = ""
+  | string [XML.Text s] = s
+  | string ts = raise XML_BODY ts;
+
+val int = int_atom o string;
+
+val bool = bool_atom o string;
+
+val unit = unit_atom o string;
+
+fun pair f g [t1, t2] = (f (node t1), g (node t2))
+  | pair _ _ ts = raise XML_BODY ts;
+
+fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
+  | triple _ _ _ ts = raise XML_BODY ts;
+
+fun list f ts = map (f o node) ts;
+
+fun option _ [] = NONE
+  | option f [t] = SOME (f (node t))
+  | option _ ts = raise XML_BODY ts;
+
+fun variant fs [t] = uncurry (nth fs) (tagged t)
+  | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
+
diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/General/xml_data.scala
--- a/src/Pure/General/xml_data.scala	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/General/xml_data.scala	Sun Jul 10 13:51:21 2011 +0200
@@ -10,150 +10,162 @@
 
 object XML_Data
 {
-  /* basic values */
+  /** make **/
 
-  class XML_Atom(s: String) extends Exception(s)
-
+  object Make
+  {
+    /* basic values */
 
-  private def make_long_atom(i: Long): String = i.toString
+    private def long_atom(i: Long): String = i.toString
+
+    private def int_atom(i: Int): String = i.toString
 
-  private def dest_long_atom(s: String): Long =
-    try { java.lang.Long.parseLong(s) }
-    catch { case e: NumberFormatException => throw new XML_Atom(s) }
+    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+    private def unit_atom(u: Unit) = ""
 
 
-  private def make_int_atom(i: Int): String = i.toString
-
-  private def dest_int_atom(s: String): Int =
-    try { Integer.parseInt(s) }
-    catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
-
-  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
+    /* structural nodes */
 
-  private def dest_bool_atom(s: String): Boolean =
-    if (s == "1") true
-    else if (s == "0") false
-    else throw new XML_Atom(s)
+    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
-
-  private def make_unit_atom(u: Unit) = ""
-
-  private def dest_unit_atom(s: String): Unit =
-    if (s == "") () else throw new XML_Atom(s)
+    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
+      XML.Elem(Markup(int_atom(tag), Nil), ts)
 
 
-  /* structural nodes */
+    /* representation of standard types */
 
-  class XML_Body(body: XML.Body) extends Exception
+    def properties(props: List[(String, String)]): XML.Body =
+      List(XML.Elem(Markup(":", props), Nil))
 
-  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+    def string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
+
+    def long(i: Long): XML.Body = string(long_atom(i))
 
-  private def dest_node(t: XML.Tree): XML.Body =
-    t match {
-      case XML.Elem(Markup(":", Nil), ts) => ts
-      case _ => throw new XML_Body(List(t))
-    }
+    def int(i: Int): XML.Body = string(int_atom(i))
+
+    def bool(b: Boolean): XML.Body = string(bool_atom(b))
 
-  private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
-    XML.Elem(Markup(make_int_atom(tag), Nil), ts)
+    def unit(u: Unit): XML.Body = string(unit_atom(u))
+
+    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)))
 
-  private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
-    t match {
-      case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
-      case _ => throw new XML_Body(List(t))
-    }
+    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)))
 
-
-  /* representation of standard types */
+    def list[A](f: A => XML.Body)(xs: List[A]): XML.Body =
+      xs.map((x: A) => node(f(x)))
 
-  def make_properties(props: List[(String, String)]): XML.Body =
-    List(XML.Elem(Markup(":", props), Nil))
+    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 dest_properties(ts: XML.Body): List[(String, String)] =
-    ts match {
-      case List(XML.Elem(Markup(":", props), Nil)) => props
-      case _ => throw new XML_Body(ts)
+    def variant[A](fs: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
+    {
+      val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+      List(tagged(tag, f(x)))
     }
+  }
+
 
 
-  def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
+  /** dest **/
+
+  class XML_Atom(s: String) extends Exception(s)
+  class XML_Body(body: XML.Body) extends Exception
+
+  object Dest
+  {
+     /* basic values */
 
-  def dest_string(ts: XML.Body): String =
-    ts match {
-      case Nil => ""
-      case List(XML.Text(s)) => s
-      case _ => throw new XML_Body(ts)
-    }
+    private def long_atom(s: String): Long =
+      try { java.lang.Long.parseLong(s) }
+      catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+    private def int_atom(s: String): Int =
+      try { Integer.parseInt(s) }
+      catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+    private def bool_atom(s: String): Boolean =
+      if (s == "1") true
+      else if (s == "0") false
+      else throw new XML_Atom(s)
+
+    private def unit_atom(s: String): Unit =
+      if (s == "") () else throw new XML_Atom(s)
 
 
-  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
-  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
-
-  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
-  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
-
-  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
-  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
+    /* structural nodes */
 
-  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
-  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
-
+    private def node(t: XML.Tree): XML.Body =
+      t match {
+        case XML.Elem(Markup(":", Nil), ts) => ts
+        case _ => throw new XML_Body(List(t))
+      }
 
-  def make_pair[A, B](make1: A => XML.Body, make2: B => XML.Body)(p: (A, B)): XML.Body =
-    List(make_node(make1(p._1)), make_node(make2(p._2)))
-
-  def dest_pair[A, B](dest1: XML.Body => A, dest2: XML.Body => B)(ts: XML.Body): (A, B) =
-    ts match {
-      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
-      case _ => throw new XML_Body(ts)
-    }
+    private def tagged(t: XML.Tree): (Int, XML.Body) =
+      t match {
+        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
+        case _ => throw new XML_Body(List(t))
+      }
 
 
-  def make_triple[A, B, C](make1: A => XML.Body, make2: B => XML.Body, make3: C => XML.Body)
-      (p: (A, B, C)): XML.Body =
-    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
+    /* 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)
+      }
 
-  def dest_triple[A, B, C](dest1: XML.Body => A, dest2: XML.Body => B, dest3: XML.Body => C)
-      (ts: XML.Body): (A, B, C) =
-    ts match {
-      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
-      case _ => 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)
+      }
 
+    def long(ts: XML.Body): Long = long_atom(string(ts))
 
-  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
-    xs.map((x: A) => make_node(make(x)))
+    def int(ts: XML.Body): Int = int_atom(string(ts))
 
-  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
-    ts.map((t: XML.Tree) => dest(dest_node(t)))
+    def bool(ts: XML.Body) = bool_atom(string(ts))
 
+    def unit(ts: XML.Body): Unit = unit_atom(string(ts))
 
-  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
-    opt match {
-      case None => Nil
-      case Some(x) => List(make_node(make(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 dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
-    ts match {
-      case Nil => None
-      case List(t) => Some(dest(dest_node(t)))
-      case _ => 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 list[A](f: XML.Body => A)(ts: XML.Body): List[A] =
+      ts.map((t: XML.Tree) => f(node(t)))
 
-  def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
-  {
-    val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
-    List(make_tagged(tag, make(x)))
-  }
+    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 dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
-    ts match {
-      case List(t) =>
-        val (tag, ts) = dest_tagged(t)
-        dests(tag)(ts)
-      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)
+      }
+  }
 }
diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 13:51:21 2011 +0200
@@ -17,21 +17,12 @@
       let
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
-        val edits =
-          XML_Data.dest_list
-            (XML_Data.dest_pair
-              XML_Data.dest_string
-              (XML_Data.dest_option
-                (XML_Data.dest_list
-                  (XML_Data.dest_pair
-                    (XML_Data.dest_option XML_Data.dest_int)
-                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
-        val headers =
-          XML_Data.dest_list
-            (XML_Data.dest_pair XML_Data.dest_string
-              (XML_Data.dest_triple XML_Data.dest_string
-                (XML_Data.dest_list XML_Data.dest_string)
-                (XML_Data.dest_list XML_Data.dest_string))) (YXML.parse_body headers_yxml);
+        val edits = YXML.parse_body edits_yxml |>
+          let open XML_Data.Dest
+          in list (pair string (option (list (pair (option int) (option int))))) end;
+        val headers = YXML.parse_body headers_yxml |>
+          let open XML_Data.Dest
+          in list (pair string (triple string (list string) (list string))) end;
 
       val await_cancellation = Document.cancel_execution state;
       val (updates, state') = Document.edit old_id new_id edits headers state;
diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:51:21 2011 +0200
@@ -143,15 +143,12 @@
       edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
   {
     val arg1 =
-      XML_Data.make_list(
-        XML_Data.make_pair(XML_Data.make_string,
-          XML_Data.make_option(XML_Data.make_list(
-              XML_Data.make_pair(
-                XML_Data.make_option(XML_Data.make_long),
-                XML_Data.make_option(XML_Data.make_long))))))(edits)
+    { import XML_Data.Make._
+      list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
 
     val arg2 =
-      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
+    { import XML_Data.Make._
+      list(pair(string, Thy_Header.make_xml_data))(headers) }
 
     input("Isar_Document.edit_version",
       Document.ID(old_id), Document.ID(new_id),
diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:51:21 2011 +0200
@@ -32,9 +32,8 @@
   }
 
   def make_xml_data(header: Header): XML.Body =
-    XML_Data.make_triple(XML_Data.make_string,
-      XML_Data.make_list(XML_Data.make_string),
-        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
+  { import XML_Data.Make._
+    triple(string, list(string), list(string))(header.name, header.imports, header.uses) }
 
 
   /* file name */
diff -r 8a63c95b1d5b -r 4e58485fa320 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 13:51:21 2011 +0200
@@ -139,8 +139,8 @@
           |> (if rem_dups then cons ("rem_dups", "") else I)
           |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
       in
-        XML.Elem (("Query", properties), XML_Data.make_list 
-          (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
+        XML.Elem (("Query", properties), XML_Data.Make.list
+          (XML_Data.Make.pair XML_Data.Make.bool (single o xml_of_criterion)) criteria)
       end
   | xml_of_query _ = raise Fail "cannot serialize goal";
 
@@ -148,8 +148,9 @@
       let
         val rem_dups = Properties.defined properties "rem_dups";
         val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
-        val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool 
-          (criterion_of_xml o the_single)) body;
+        val criteria =
+          XML_Data.Dest.list (XML_Data.Dest.pair XML_Data.Dest.bool 
+            (criterion_of_xml o the_single)) body;
       in
         {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
       end
@@ -189,12 +190,12 @@
     val properties =
       if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   in
-    XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
+    XML.Elem (("Result", properties), XML_Data.Make.list (single o xml_of_theorem) theorems)
   end;
 
 fun result_of_xml (XML.Elem (("Result", properties), body)) =
       (Properties.get properties "found" |> Option.map Markup.parse_int,
-       XML_Data.dest_list (theorem_of_xml o the_single) body)
+       XML_Data.Dest.list (theorem_of_xml o the_single) body)
   | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
 
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm