src/Tools/Haskell/Haskell.thy
changeset 69236 a75aab6d785b
parent 69234 2dec32c7313f
child 69240 16ca270090b6
     1.1 --- a/src/Tools/Haskell/Haskell.thy	Mon Nov 05 10:02:21 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Mon Nov 05 11:29:11 2018 +0100
     1.3 @@ -481,16 +481,12 @@
     1.4  
     1.5  {- wrapped elements -}
     1.6  
     1.7 -xml_elemN = \<open>XML.xml_elemN\<close>
     1.8 -xml_nameN = \<open>XML.xml_nameN\<close>
     1.9 -xml_bodyN = \<open>XML.xml_bodyN\<close>
    1.10 +wrap_elem (((a, atts), body1), body2) =
    1.11 +  Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)
    1.12  
    1.13 -wrap_elem (((a, atts), body1), body2) =
    1.14 -  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
    1.15 -
    1.16 -unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
    1.17 -  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
    1.18 -  then Just (((a, atts), body1), body2) else Nothing
    1.19 +unwrap_elem
    1.20 +  (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
    1.21 +  Just (((a, atts), body1), body2)
    1.22  unwrap_elem _ = Nothing
    1.23  
    1.24