diff -r 877f0c44d77e -r 9fcf09cf7b36 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jan 19 10:11:24 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 20 13:53:13 2022 +0100
@@ -532,14 +532,14 @@
           val tm1' = traverse tm1
           val tm2' = traverse tm2
         in
-          if tm1 = tm1' andalso tm2 = tm2' then tm else IApp (tm1', tm2')
+          if pointer_eq (tm1, tm1') andalso pointer_eq (tm2, tm2') then tm else IApp (tm1', tm2')
         end
       | traverse (tm as IAbs (binding as (name, _), tm1)) =
         if name = from then
           tm
         else
           let val tm1' = traverse tm1 in
-            if tm1 = tm1' then tm else IAbs (binding, tm1')
+            if pointer_eq (tm1, tm1') then tm else IAbs (binding, tm1')
           end
   in
     traverse