# HG changeset patch
# User wenzelm
# Date 1725918428 -7200
# Node ID ddc062eac8712ec9766fa4189ad7afbf91d363d8
# Parent  7f989a84284ae66597832e2a443c86c6b139f055
tuned;

diff -r 7f989a84284a -r ddc062eac871 src/Pure/PIDE/xml_type.ML
--- a/src/Pure/PIDE/xml_type.ML	Mon Sep 09 23:45:45 2024 +0200
+++ b/src/Pure/PIDE/xml_type.ML	Mon Sep 09 23:47:08 2024 +0200
@@ -40,8 +40,8 @@
 fun wrap_elem (((a, atts), body1), body2) =
   Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
 
-fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
-      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
+fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', []), body1) :: body2)) =
+      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN
       then SOME (((a, atts), body1), body2) else NONE
   | unwrap_elem _ = NONE;