# HG changeset patch
# User wenzelm
# Date 1725918345 -7200
# Node ID 7f989a84284ae66597832e2a443c86c6b139f055
# Parent  abe1661ad6920a7937acd11784d5dca3e045ac1d
tuned signature;

diff -r abe1661ad692 -r 7f989a84284a src/Pure/PIDE/xml_type.ML
--- a/src/Pure/PIDE/xml_type.ML	Mon Sep 09 22:59:51 2024 +0200
+++ b/src/Pure/PIDE/xml_type.ML	Mon Sep 09 23:45:45 2024 +0200
@@ -14,8 +14,8 @@
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
-  val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
-  val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
+  val wrap_elem: ((string * attributes) * body) * body -> tree
+  val unwrap_elem: tree -> (((string * attributes) * body) * body) option
   val content_of: body -> string
 end