--- 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;