diff --git a/ismm/FStar.Mul.fst b/ismm/FStar.Mul.fst
new file mode 100644
index 00000000..368e7121
--- /dev/null
+++ b/ismm/FStar.Mul.fst
@@ -0,0 +1,6 @@
+module FStar.Mul
+
+// Compatibility shim: FStar.Mul was removed in F* nightly-2026-04-29.
+// The multiplication operator is now op_Star rather than op_Multiply.
+
+let op_Multiply (x y: int) : int = x * y
diff --git a/ismm/ISMM.UF.SizeRank.fst b/ismm/ISMM.UF.SizeRank.fst
index 4709a9bf..d1ebd55f 100644
--- a/ismm/ISMM.UF.SizeRank.fst
+++ b/ismm/ISMM.UF.SizeRank.fst
@@ -8,6 +8,7 @@
 module ISMM.UF.SizeRank
 
 open FStar.Seq
+open FStar.Mul
 module Seq = FStar.Seq
 open ISMM.UnionFind.Spec
 
diff --git a/ismm/ISMM.UnionFind.Spec.fst b/ismm/ISMM.UnionFind.Spec.fst
index 32c6c8af..eb2b3730 100644
--- a/ismm/ISMM.UnionFind.Spec.fst
+++ b/ismm/ISMM.UnionFind.Spec.fst
@@ -17,6 +17,7 @@
 module ISMM.UnionFind.Spec
 
 open FStar.Seq
+open FStar.Mul
 module Seq = FStar.Seq
 open ISMM.Status