--- 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,
--- 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 *)