changeset 71777 | 3875815f5967 |
parent 71553 | cf2406e654cf |
child 73860 | dfac078e5444 |
--- a/src/Pure/thm.ML Tue Apr 21 22:04:15 2020 +0200 +++ b/src/Pure/thm.ML Tue Apr 21 22:19:59 2020 +0200 @@ -1719,7 +1719,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.OfClass (T, c)), + Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c)), {cert = cert, tags = [], maxidx = maxidx,