diff -r 2acdaa0a7d29 -r 446b887e23c7 src/Pure/term_xml.ML
--- 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;