src/Tools/Haskell/Haskell.thy

   else (Markup.empty, [])
 
 markup_report :: [T] -> String
 markup_report [] = ""
 markup_report elems =
-  elems
-  |> map (markup_element #> uncurry XML.Elem)
-  |> XML.Elem Markup.report
-  |> YXML.string_of
+  YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
 
 make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
 make_report limit name_props make_names =
   markup_report [make limit name_props make_names]
 \<close>

 
 {- types -}
 
 type Attributes = Properties.T
 type Body = [Tree]
-data Tree = Elem Markup.T Body | Text String
+data Tree = Elem (Markup.T, Body) | Text String
 
 
 {- wrapped elements -}
 
 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)
+  Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)
 
 unwrap_elem
-  (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
+  (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
 
 
 {- text content -}

 add_content tree =
   case unwrap_elem tree of
     Just (_, ts) -> fold add_content ts
     Nothing ->
       case tree of
-        Elem _ ts -> fold add_content ts
+        Elem (_, ts) -> fold add_content ts
         Text s -> Buffer.add s
 
 content_of body = Buffer.empty |> fold add_content body |> Buffer.content
 
 

 
 instance Show Tree where
   show tree =
     Buffer.empty |> show_tree tree |> Buffer.content
     where
-      show_tree (Elem (name, atts) []) =
+      show_tree (Elem ((name, atts), [])) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
-      show_tree (Elem (name, atts) ts) =
+      show_tree (Elem ((name, atts), ts)) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
         fold show_tree ts #>
         Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
       show_tree (Text s) = Buffer.add (show_text s)
 

 unit_atom () = ""
 
 
 -- structural nodes
 
-node = XML.Elem (":", [])
+node ts = XML.Elem ((":", []), ts)
 
 vector = map_index (\(i, x) -> (int_atom i, x))
 
-tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
+tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
 
 
 -- representation of standard types
 
 tree :: T XML.Tree
 tree t = [t]
 
 properties :: T Properties.T
-properties props = [XML.Elem (":", props) []]
+properties props = [XML.Elem ((":", props), [])]
 
 string :: T String
 string "" = []
 string s = [XML.Text s]
 

 unit_atom _ = err_atom
 
 
 {- structural nodes -}
 
-node (XML.Elem (":", []) ts) = ts
+node (XML.Elem ((":", []), ts)) = ts
 node _ = err_body
 
 vector atts =
   map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
 
-tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
+tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
 tagged _ = err_body
 
 
 {- representation of standard types -}
 
 tree :: T XML.Tree
 tree [t] = t
 tree _ = err_body
 
 properties :: T Properties.T
-properties [XML.Elem (":", props) []] = props
+properties [XML.Elem ((":", props), [])] = props
 properties _ = err_body
 
 string :: T String
 string [] = ""
 string [XML.Text s] = s

 
 buffer_body :: XML.Body -> Buffer.T -> Buffer.T
 buffer_body = fold buffer
 
 buffer :: XML.Tree -> Buffer.T -> Buffer.T
-buffer (XML.Elem (name, atts) ts) =
+buffer (XML.Elem ((name, atts), ts)) =
   Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   buffer_body ts #>
   Buffer.add strXYX
 buffer (XML.Text s) = Buffer.add s
 

 
 push "" _ _ = err_element
 push name atts pending = ((name, atts), []) : pending
 
 pop ((("", _), _) : _) = err_unbalanced ""
-pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
+pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
 
 
 -- parsing
 
 parse_attrib s =

 symbolic_text "" = []
 symbolic_text s = [XML.Text s]
 
 symbolic_markup markup body =
   if Markup.is_empty markup then body
-  else [XML.Elem markup body]
+  else [XML.Elem (markup, body)]
 
 symbolic :: T -> XML.Body
 symbolic (Block markup consistent indent prts) =
   concatMap symbolic prts
   |> symbolic_markup block_markup
   |> symbolic_markup markup
   where block_markup = if null prts then Markup.empty else Markup.block consistent indent
-symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
+symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
 symbolic (Str s) = symbolic_text s
 
 formatted :: T -> String
 formatted = YXML.string_of_body . symbolic