# HG changeset patch
# User wenzelm
# Date 1570822477 -7200
# Node ID 874092c031c30267993f3a9a3b12c9b6ca18227c
# Parent  44efbf2525254e862ad2d147889e5eff89badbbd
tuned signature;

diff -r 44efbf252525 -r 874092c031c3 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 21:23:06 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 11 21:34:37 2019 +0200
@@ -15,6 +15,7 @@
   val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
   val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
   val expand_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+  val expand_of_class_proof : theory -> term option list -> typ * class -> proof
   val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
     (Proofterm.proof * Proofterm.proof) option
 end;
@@ -366,8 +367,11 @@
         (OfClass o apfst Type.strip_sorts) (subst T, S))
   end;
 
-fun expand_of_class thy (_: typ list) hs (OfClass (T, c)) =
-      SOME (expand_of_sort_proof thy hs (T, [c]) |> hd, Proofterm.no_skel)
+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)) =
+      SOME (expand_of_class_proof thy hyps (T, c), Proofterm.no_skel)
   | expand_of_class _ _ _ _ = NONE;
 
 end;