# HG changeset patch
# User wenzelm
# Date 1704022810 -3600
# Node ID cb19148c0b958beeb0a3f61925243f8c8d6e5843
# Parent  254b062ec54dac5e31df11ef60f7a30f47d1a743
tuned comments;

diff -r 254b062ec54d -r cb19148c0b95 src/Pure/logic.ML
--- 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);
 
diff -r 254b062ec54d -r cb19148c0b95 src/Pure/proofterm.ML
--- 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
diff -r 254b062ec54d -r cb19148c0b95 src/Pure/thm.ML
--- 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