src/Pure/thm.ML

       handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE);
     val c = Sign.certify_class thy raw_c;
     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,
         constraints = insert_constraints thy (T, [c]) [],
         shyps = sorts,