diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/SPARK/Manual/Reference.thy
--- a/src/HOL/SPARK/Manual/Reference.thy	Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Sun Aug 01 10:20:34 2021 +0000
@@ -3,6 +3,8 @@
 imports "HOL-SPARK.SPARK"
 begin
 
+unbundle bit_operations_syntax
+
 lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n" for x :: int
   by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod)