src/Pure/PIDE/xml.ML
changeset 80838 aaf9e8a392cc
parent 80820 db114ec720cb
child 80847 93c2058896a4
--- a/src/Pure/PIDE/xml.ML	Mon Sep 09 23:47:08 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Mon Sep 09 23:50:58 2024 +0200
@@ -96,8 +96,8 @@
 (* text content *)
 
 fun add_content tree =
-  (case unwrap_elem tree of
-    SOME (_, ts) => fold add_content ts
+  (case unwrap_elem_body tree of
+    SOME ts => fold add_content ts
   | NONE =>
       (case tree of
         Elem (_, ts) => fold add_content ts