# HG changeset patch
# User wenzelm
# Date 1701772644 -3600
# Node ID b6f5d439238896720d1fca9a636ebf55b8fff7e6
# Parent  830f68f92ad7ec0e1a8407cbab8c4271f205e426
more zproofs;

diff -r 830f68f92ad7 -r b6f5d4392388 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 05 11:11:00 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 05 11:37:24 2023 +0100
@@ -1878,7 +1878,7 @@
     val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
   in
     if Sign.of_sort thy (T, [c]) then
-      Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c), ZTerm.todo_proof),
+      Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c), fn () => ZTerm.of_class_proof (T, c)),
        {cert = cert,
         tags = [],
         maxidx = maxidx,
diff -r 830f68f92ad7 -r b6f5d4392388 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 05 11:11:00 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 05 11:37:24 2023 +0100
@@ -171,6 +171,7 @@
   val implies_intr_proof: theory -> term -> zproof -> zproof
   val forall_intr_proof: theory -> typ -> string * term -> zproof -> zproof
   val forall_elim_proof: theory -> term -> zproof -> zproof
+  val of_class_proof: typ * class -> zproof
   val reflexive_proof: theory -> typ -> term -> zproof
   val symmetric_proof: theory -> typ -> term -> term -> zproof -> zproof
   val transitive_proof: theory -> typ -> term -> term -> term -> zproof -> zproof -> zproof
@@ -328,6 +329,8 @@
 
 fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t);
 
+fun of_class_proof (T, c) = ZClassP (ztyp_of T, c);
+
 
 (* equality *)