# HG changeset patch
# User wenzelm
# Date 1570875916 -7200
# Node ID c5caf81aa5237229b653e8557f446eeb2878ff9f
# Parent  3d8953224f33e147187ce88cc5369d516f127872
more compact XML;

diff -r 3d8953224f33 -r c5caf81aa523 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Fri Oct 11 22:06:49 2019 +0200
+++ b/src/Pure/term_xml.ML	Sat Oct 12 12:25:16 2019 +0200
@@ -10,9 +10,9 @@
   type 'a P
   val indexname: indexname P
   val sort: sort T
-  val typ_raw: typ T
+  val typ: typ T
   val term_raw: term T
-  val typ: typ T
+  val typ_body: typ T
   val term: Consts.T -> term T
 end
 
@@ -34,25 +34,25 @@
 
 val sort = list string;
 
-fun typ_raw T = T |> variant
- [fn Type (a, b) => ([a], list typ_raw b),
+fun typ T = T |> variant
+ [fn Type (a, b) => ([a], list typ b),
   fn TFree (a, b) => ([a], sort b),
   fn TVar (a, b) => (indexname a, sort b)];
 
 fun term_raw t = t |> variant
- [fn Const (a, b) => ([a], typ_raw b),
-  fn Free (a, b) => ([a], typ_raw b),
-  fn Var (a, b) => (indexname a, typ_raw b),
+ [fn Const (a, b) => ([a], typ b),
+  fn Free (a, b) => ([a], typ b),
+  fn Var (a, b) => (indexname a, typ b),
   fn Bound a => ([int_atom a], []),
-  fn Abs (a, b, c) => ([a], pair typ_raw term_raw (b, c)),
+  fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
   fn op $ a => ([], pair term_raw term_raw a)];
 
-fun typ T = option typ_raw (if T = dummyT then NONE else SOME T);
+fun typ_body T = if T = dummyT then [] else typ T;
 
 fun term consts t = t |> variant
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
-  fn Free (a, b) => ([a], typ b),
-  fn Var (a, b) => (indexname a, typ b),
+  fn Free (a, b) => ([a], typ_body b),
+  fn Var (a, b) => (indexname a, typ_body b),
   fn Bound a => ([int_atom a], []),
   fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
   fn op $ a => ([], pair (term consts) (term consts) a)];
@@ -69,25 +69,26 @@
 
 val sort = list string;
 
-fun typ_raw body = body |> variant
- [fn ([a], b) => Type (a, list typ_raw b),
+fun typ body = body |> variant
+ [fn ([a], b) => Type (a, list typ b),
   fn ([a], b) => TFree (a, sort b),
   fn (a, b) => TVar (indexname a, sort b)];
 
 fun term_raw body = body |> variant
- [fn ([a], b) => Const (a, typ_raw b),
-  fn ([a], b) => Free (a, typ_raw b),
-  fn (a, b) => Var (indexname a, typ_raw b),
+ [fn ([a], b) => Const (a, typ b),
+  fn ([a], b) => Free (a, typ b),
+  fn (a, b) => Var (indexname a, typ b),
   fn ([a], []) => Bound (int_atom a),
-  fn ([a], b) => let val (c, d) = pair typ_raw term_raw b in Abs (a, c, d) end,
+  fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair term_raw term_raw a)];
 
-val typ = option typ_raw #> the_default dummyT;
+fun typ_body [] = dummyT
+  | typ_body body = typ body;
 
 fun term consts body = body |> variant
  [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
-  fn ([a], b) => Free (a, typ b),
-  fn (a, b) => Var (indexname a, typ b),
+  fn ([a], b) => Free (a, typ_body b),
+  fn (a, b) => Var (indexname a, typ_body b),
   fn ([a], []) => Bound (int_atom a),
   fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair (term consts) (term consts) a)];
diff -r 3d8953224f33 -r c5caf81aa523 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Fri Oct 11 22:06:49 2019 +0200
+++ b/src/Pure/term_xml.scala	Sat Oct 12 12:25:16 2019 +0200
@@ -21,20 +21,19 @@
 
     val sort: T[Sort] = list(string)
 
-    def typ_raw: T[Typ] =
+    def typ: T[Typ] =
       variant[Typ](List(
-        { case Type(a, b) => (List(a), list(typ_raw)(b)) },
+        { case Type(a, b) => (List(a), list(typ)(b)) },
         { case TFree(a, b) => (List(a), sort(b)) },
         { case TVar(a, b) => (indexname(a), sort(b)) }))
 
-    val typ: T[Typ] =
-      { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) }
+    val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
 
     def term: T[Term] =
       variant[Term](List(
         { case Const(a, b) => (List(a), list(typ)(b)) },
-        { case Free(a, b) => (List(a), typ(b)) },
-        { case Var(a, b) => (indexname(a), typ(b)) },
+        { case Free(a, b) => (List(a), typ_body(b)) },
+        { case Var(a, b) => (indexname(a), typ_body(b)) },
         { case Bound(a) => (List(int_atom(a)), Nil) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
@@ -50,19 +49,19 @@
 
     val sort: T[Sort] = list(string)
 
-    def typ_raw: T[Typ] =
+    def typ: T[Typ] =
       variant[Typ](List(
-        { case (List(a), b) => Type(a, list(typ_raw)(b)) },
+        { case (List(a), b) => Type(a, list(typ)(b)) },
         { case (List(a), b) => TFree(a, sort(b)) },
         { case (a, b) => TVar(indexname(a), sort(b)) }))
 
-    def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT)
+    val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
 
     def term: T[Term] =
       variant[Term](List(
         { case (List(a), b) => Const(a, list(typ)(b)) },
-        { case (List(a), b) => Free(a, typ(b)) },
-        { case (a, b) => Var(indexname(a), typ(b)) },
+        { case (List(a), b) => Free(a, typ_body(b)) },
+        { case (a, b) => Var(indexname(a), typ_body(b)) },
         { case (List(a), Nil) => Bound(int_atom(a)) },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))