diff -r 6cd985a78d6e -r 16ca270090b6 src/Tools/Haskell/Term_XML/Decode.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Haskell/Term_XML/Decode.hs	Mon Nov 05 17:06:50 2018 +0100
@@ -0,0 +1,37 @@
+{- generated by Isabelle -}
+
+{-  Title:      Tools/Haskell/Term_XML/Decode.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+XML data representation of lambda terms.
+-}
+
+module Isabelle.Term_XML.Decode (sort, typ, term)
+where
+
+import Isabelle.Library
+import qualified Isabelle.XML as XML
+import Isabelle.XML.Decode
+import Isabelle.Term
+
+
+sort :: T Sort
+sort = list string
+
+typ :: T Typ
+typ ty =
+  ty |> variant
+  [\([a], b) -> Type (a, list typ b),
+   \([a], b) -> TFree (a, sort b),
+   \([a, b], c) -> TVar ((a, int_atom b), sort c)]
+
+term :: T Term
+term t =
+  t |> variant
+   [\([a], b) -> Const (a, typ b),
+    \([a], b) -> Free (a, typ b),
+    \([a, b], c) -> Var ((a, int_atom b), typ c),
+    \([a], []) -> Bound (int_atom a),
+    \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
+    \([], a) -> App (pair term term a)]