diff --git a/theories/TM/Single/StepTM.v b/theories/TM/Single/StepTM.v
index f78d5a18..d9fcccb8 100644
--- a/theories/TM/Single/StepTM.v
+++ b/theories/TM/Single/StepTM.v
@@ -384,7 +384,7 @@ Section ToSingleTape.
   Notation nMax := (finMax' n).
   Local Arguments finMax' : simpl never.
 
-  Notation sigSim := (FinType(EqType(boundary + sigList (sigTape sig)))).
+  Definition sigSim := (FinType(EqType(boundary + sigList (sigTape sig)))).
 
   Implicit Types (T : tapes sig n).