# HG changeset patch
# User wenzelm
# Date 1570885273 -7200
# Node ID f95a85446a24a91b4cfdb9e0c5dd6881c00bd0a6
# Parent  cc987440d77622987ff687bb47aa22ab2b231de8
more compact XML;

diff -r cc987440d776 -r f95a85446a24 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Oct 12 13:43:17 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Oct 12 15:01:13 2019 +0200
@@ -333,7 +333,7 @@
 
 fun proof consts prf = prf |> variant
  [fn MinProof => ([], []),
-  fn PBound a => ([int_atom a], []),
+  fn PBound a => ([], int a),
   fn Abst (a, b, c) => ([a], pair (option typ) (proof consts) (b, c)),
   fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)),
   fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)),
@@ -358,13 +358,13 @@
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
   fn Free (a, _) => ([a], []),
   fn Var (a, _) => (indexname a, []),
-  fn Bound a => ([int_atom a], []),
+  fn Bound a => ([], int a),
   fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
   fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)];
 
 fun standard_proof consts prf = prf |> variant
  [fn MinProof => ([], []),
-  fn PBound a => ([int_atom a], []),
+  fn PBound a => ([], int a),
   fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
   fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)),
   fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)),
@@ -394,7 +394,7 @@
 
 fun proof consts prf = prf |> variant
  [fn ([], []) => MinProof,
-  fn ([a], []) => PBound (int_atom a),
+  fn ([], a) => PBound (int a),
   fn ([a], b) => let val (c, d) = pair (option typ) (proof consts) b in Abst (a, c, d) end,
   fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end,
   fn ([], a) => op % (pair (proof consts) (option (term consts)) a),
diff -r cc987440d776 -r f95a85446a24 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Sat Oct 12 13:43:17 2019 +0200
+++ b/src/Pure/term_xml.ML	Sat Oct 12 15:01:13 2019 +0200
@@ -43,7 +43,7 @@
  [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 Bound a => ([], int a),
   fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
   fn op $ a => ([], pair term_raw term_raw a)];
 
@@ -53,7 +53,7 @@
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, 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 Bound a => ([], int a),
   fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
   fn op $ a => ([], pair (term consts) (term consts) a)];
 
@@ -78,7 +78,7 @@
  [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) => Bound (int a),
   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)];
 
@@ -89,7 +89,7 @@
  [fn ([a], b) => Const (a, Consts.instance consts (a, list 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) => Bound (int 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 cc987440d776 -r f95a85446a24 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Sat Oct 12 13:43:17 2019 +0200
+++ b/src/Pure/term_xml.scala	Sat Oct 12 15:01:13 2019 +0200
@@ -34,7 +34,7 @@
         { case Const(a, b) => (List(a), list(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 Bound(a) => (Nil, int(a)) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
   }
@@ -62,7 +62,7 @@
         { case (List(a), b) => Const(a, list(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 (Nil, a) => Bound(int(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) }))
 
@@ -76,7 +76,7 @@
           { case (List(a), b) => Const(a, list(typ)(b)) },
           { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
           { case (a, b) => Var(indexname(a), typ_body(b)) },
-          { case (List(a), Nil) => Bound(int_atom(a)) },
+          { case (Nil, a) => Bound(int(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) }))
       term
@@ -88,7 +88,7 @@
       def proof: T[Proof] =
         variant[Proof](List(
           { case (Nil, Nil) => MinProof },
-          { case (List(a), Nil) => PBound(int_atom(a)) },
+          { case (Nil, a) => PBound(int(a)) },
           { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
           { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
           { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },