src/Pure/Proof/proof_rewrite_rules.ML

       Proofterm.reconstruct_proof thy prop |>
       Proofterm.expand_proof thy [("", NONE)] |>
       Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
   in
     map2 reconstruct
-      (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst 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))
       (Logic.mk_of_sort (T, S))
   end;
 
 fun expand_of_class thy Ts hs (OfClass (T, c)) =
       mk_of_sort_proof thy hs (T, [c]) |>