--- a/src/Pure/logic.ML Sun Dec 31 12:33:13 2023 +0100
+++ b/src/Pure/logic.ML Sun Dec 31 12:40:10 2023 +0100
@@ -350,7 +350,7 @@
in (t, Ss, c) end;
-(* internalized sort constraints *)
+(* sort constraints within the logic *)
fun dummy_tfree S = TFree ("'dummy", S);
--- a/src/Pure/proofterm.ML Sun Dec 31 12:33:13 2023 +0100
+++ b/src/Pure/proofterm.ML Sun Dec 31 12:40:10 2023 +0100
@@ -1095,7 +1095,7 @@
-(** type classes **)
+(** sort constraints within the logic **)
fun of_sort_proof algebra classrel_proof arity_proof hyps =
Sorts.of_sort_derivation algebra
--- a/src/Pure/thm.ML Sun Dec 31 12:33:13 2023 +0100
+++ b/src/Pure/thm.ML Sun Dec 31 12:40:10 2023 +0100
@@ -2004,7 +2004,7 @@
else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
end |> solve_constraints;
-(*Internalize sort constraints of type variables*)
+(*Sort constraints within the logic*)
val unconstrainT =
strip_shyps #> (fn thm as Thm (der, args) =>
let