some treatment of OfClass proofs;
authorwenzelm
Fri, 11 Oct 2019 21:44:39 +0200
changeset 71028 e381e2624077
parent 71027 874092c031c3
child 71029 2136e4670ad2
some treatment of OfClass proofs;
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