diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun May 18 14:33:01 2025 +0000
@@ -306,9 +306,9 @@
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
 fun list_of_Int th =
     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
-    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+    handle THM _ => (list_of_Int (th RS @{thm IntD1}) @ list_of_Int (th RS @{thm IntD2}))
     handle THM _ => (list_of_Int (th RS @{thm INT_D}))
-    handle THM _ => (list_of_Int (th RS bspec))
+    handle THM _ => (list_of_Int (th RS @{thm bspec}))
     handle THM _ => [th];
 \<close>
 
@@ -319,7 +319,7 @@
   fun normalized th =
     normalized (th RS spec
       handle THM _ => th RS @{thm lessThanBspec}
-      handle THM _ => th RS bspec
+      handle THM _ => th RS @{thm bspec}
       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
     handle THM _ => th;
 in