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)];