# HG changeset patch
# User wenzelm
# Date 1541413751 -3600
# Node ID a75aab6d785b39a3e9e45e9f0e3b2c937bfeeadd
# Parent  0e156963b636f135396359a88036a8cb9e83f9e4
tuned;

diff -r 0e156963b636 -r a75aab6d785b src/Tools/Haskell/Haskell.thy
--- 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
 
 
diff -r 0e156963b636 -r a75aab6d785b src/Tools/Haskell/XML.hs
--- 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