--- a/src/Pure/unify.ML Wed Dec 06 22:03:14 2023 +0100
+++ b/src/Pure/unify.ML Thu Dec 07 09:34:07 2023 +0100
@@ -68,7 +68,7 @@
(*OCCURS CHECK
Does the uvar occur in the term t?
two forms of search, for whether there is a rigid path to the current term.
- "seen" is list of variables passed thru, is a memo variable for sharing.
+ "seen" is list of variables passed through, is a memo variable for sharing.
This version searches for nonrigid occurrence, returns true if found.
Since terms may contain variables with same name and different types,
the occurs check must ignore the types of variables. This avoids