--- 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;
+
--- 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)
+ }
+ }
}
--- 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;
--- 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),
--- 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 */
--- 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