--- a/src/Pure/Proof/proof_checker.ML Fri Oct 11 21:34:37 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML Fri Oct 11 21:44:39 2019 +0200
@@ -137,6 +137,13 @@
| thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t)
+ | thm_of _ _ (OfClass (T, c)) =
+ if Sign.of_sort thy (T, [c])
+ then Thm.of_class (Thm.global_ctyp_of thy T, c)
+ else
+ error ("thm_of_proof: bad OfClass proof " ^
+ Syntax.string_of_term_global thy (Logic.mk_of_class (T, c)))
+
| thm_of _ _ _ = error "thm_of_proof: partial proof term";
in beta_eta_convert (thm_of ([], prf_names) [] prf) end