--- a/src/HOL/Types_To_Sets/internalize_sort.ML Sat Dec 30 15:50:18 2023 +0100
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML Sat Dec 30 15:59:11 2023 +0100
@@ -31,14 +31,14 @@
val thy = Thm.theory_of_thm thm;
val tvar = Thm.typ_of ctvar;
- val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm);
+ val ({constraints, outer_constraints, ...}, _) = Logic.unconstrainT [] (Thm.prop_of thm);
fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
fun reduce_to_non_proper_sort (TVar (name, sort)) =
TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
| reduce_to_non_proper_sort _ = error "not supported";
- val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext;
+ val data = map #1 outer_constraints ~~ constraints;
val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data