--- a/src/Pure/term_xml.ML Sun Jul 14 16:17:31 2024 +0200
+++ b/src/Pure/term_xml.ML Sun Jul 14 17:49:30 2024 +0200
@@ -55,7 +55,12 @@
fn Var (a, b) => (indexname a, typ_body b),
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)];
+ fn t as op $ a =>
+ if can Logic.match_of_class t then raise Match
+ else ([], pair (term consts) (term consts) a),
+ fn t =>
+ let val (T, c) = Logic.match_of_class t
+ in ([c], typ T) end];
end;
@@ -91,7 +96,8 @@
fn (a, b) => Var (indexname a, typ_body b),
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)];
+ fn ([], a) => op $ (pair (term consts) (term consts) a),
+ fn ([a], b) => Logic.mk_of_class (typ b, a)];
end;