diff -r f12539c8de0c -r 18cd39e55eca src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Feb 22 12:45:14 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Feb 22 15:00:04 2022 +0100
@@ -409,8 +409,9 @@
     val long = Thm.get_name_hint th
     val short = Long_Name.base_name long
   in
-    if Thm.eq_thm_prop (th, singleton (Attrib.eval_thms ctxt) (Facts.named short, [])) then short
-    else long
+    (case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of
+      SOME th' => if Thm.eq_thm_prop (th, th') then short else long
+    | _ => long)
   end
 
 val map_prod = Ctr_Sugar_Util.map_prod