src/Pure/zterm.ML

--- a/src/Pure/zterm.ML	Fri Dec 01 18:12:18 2023 +0100
+++ b/src/Pure/zterm.ML	Sat Dec 02 15:42:50 2023 +0100
@@ -56,6 +56,8 @@
   val typ_of: ztyp -> typ
   val zterm_of: Consts.T -> term -> zterm
   val term_of: Consts.T -> zterm -> term
+  val dummy_proof: 'a -> zproof
+  val todo_proof: 'a -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -168,4 +170,10 @@
       | term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c);
   in term end;
 
+
+(* proofs *)
+
+fun dummy_proof _ = ZDummy;
+val todo_proof = dummy_proof;
+
 end;