# HG changeset patch
# User wenzelm
# Date 1570823079 -7200
# Node ID e381e2624077c62f2f8a580e4b9b2aa34ea30ec7
# Parent  874092c031c30267993f3a9a3b12c9b6ca18227c
some treatment of OfClass proofs;

diff -r 874092c031c3 -r e381e2624077 src/Pure/Proof/proof_checker.ML
--- 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