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