--- a/src/Tools/Haskell/Haskell.thy Mon Nov 05 10:02:21 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Mon Nov 05 11:29:11 2018 +0100
@@ -481,16 +481,12 @@
{- wrapped elements -}
-xml_elemN = \<open>XML.xml_elemN\<close>
-xml_nameN = \<open>XML.xml_nameN\<close>
-xml_bodyN = \<open>XML.xml_bodyN\<close>
+wrap_elem (((a, atts), body1), body2) =
+ Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)
-wrap_elem (((a, atts), body1), body2) =
- Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
-
-unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
- if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
- then Just (((a, atts), body1), body2) else Nothing
+unwrap_elem
+ (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
+ Just (((a, atts), body1), body2)
unwrap_elem _ = Nothing
--- a/src/Tools/Haskell/XML.hs Mon Nov 05 10:02:21 2018 +0100
+++ b/src/Tools/Haskell/XML.hs Mon Nov 05 11:29:11 2018 +0100
@@ -27,16 +27,12 @@
{- wrapped elements -}
-xml_elemN = "xml_elem"
-xml_nameN = "xml_name"
-xml_bodyN = "xml_body"
+wrap_elem (((a, atts), body1), body2) =
+ Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)
-wrap_elem (((a, atts), body1), body2) =
- Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
-
-unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
- if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
- then Just (((a, atts), body1), body2) else Nothing
+unwrap_elem
+ (Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)) =
+ Just (((a, atts), body1), body2)
unwrap_elem _ = Nothing