diff -r 5109e4b2a292 -r 686b7b14d041 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/zterm.ML	Sat Dec 02 19:57:57 2023 +0100
@@ -38,11 +38,6 @@
   | ZAppP of zproof * zproof
   | ZClassP of ztyp * class        (*OFCLASS proof from sorts algebra*)
   | ZOracle of serial * zterm * ztyp list
-and zproof_body = ZPBody of
-  {boxes: (zterm * zproof future) Inttab.table,
-   consts: serial Ord_List.T,
-   oracles: ((string * Position.T) * zterm option) Ord_List.T,
-   proof: zproof}
 
 
 signature ZTERM =