--- a/src/Pure/Proof/proof_rewrite_rules.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sun Dec 31 22:04:41 2023 +0100
@@ -264,8 +264,7 @@
fun elim_defs thy r defs prf =
let
- val defs' = map (Logic.dest_equals o
- map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
+ val defs' = map (Logic.dest_equals o Term.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
val defnames = map Thm.derivation_name defs;
val prf' =
if r then
@@ -375,7 +374,7 @@
in
map2 reconstruct (Logic.mk_of_sort (T, S))
(Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.sorts_proof thy)
- (PClass o apfst Type.strip_sorts) (subst T, S))
+ (PClass o apfst Term.strip_sortsT) (subst T, S))
end;
fun expand_of_class_proof thy hyps (T, c) =