src/Pure/Proof/proof_rewrite_rules.ML

       (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
     mk_prf Q
   end;
 
 
-(**** expand OfClass proofs ****)
+(**** expand PClass proofs ****)
 
 fun expand_of_sort_proof thy hyps (T, S) =
   let
     val of_class_hyps = map (fn SOME t => try Logic.dest_of_class t | NONE => NONE) hyps;
     fun of_class_index p =

       Proofterm.expand_proof thy Proofterm.expand_name_empty #>
       Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index);
   in
     map2 reconstruct (Logic.mk_of_sort (T, S))
       (Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.classrel_proof thy) (Thm.arity_proof thy)
-        (OfClass o apfst Type.strip_sorts) (subst T, S))
+        (PClass o apfst Type.strip_sorts) (subst T, S))
   end;
 
 fun expand_of_class_proof thy hyps (T, c) =
   hd (expand_of_sort_proof thy hyps (T, [c]));
 
-fun expand_of_class thy (_: typ list) hyps (OfClass (T, c)) =
+fun expand_of_class thy (_: typ list) hyps (PClass (T, c)) =
       SOME (expand_of_class_proof thy hyps (T, c), Proofterm.no_skel)
   | expand_of_class _ _ _ _ = NONE;
 
 
 (* standard preprocessor *)