diff --git a/docs/CryptolPrims.markdown b/docs/CryptolPrims.markdown
index 4c31bf04..943cf309 100644
--- a/docs/CryptolPrims.markdown
+++ b/docs/CryptolPrims.markdown
@@ -6,7 +6,7 @@ Old types:
     (==)   : {a}   (fin a) => (a,a) -> Bit
     (!=)   : {a}   (fin a) => (a,a) -> Bit
     (===)  : {a b} (fin b) => (a -> b,a -> b) -> a -> Bit
-    (!===) : {a b} (fin b) => (a -> b,a -> b) -> a -> Bit
+    (!==)  : {a b} (fin b) => (a -> b,a -> b) -> a -> Bit
 
     (<)    : {n} (fin n) => ([n],[n]) -> Bit
     (>)    : {n} (fin n) => ([n],[n]) -> Bit
diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y
index 9a3a80f3..093f4d99 100644
--- a/src/Cryptol/Parser.y
+++ b/src/Cryptol/Parser.y
@@ -114,7 +114,7 @@ import Paths_cryptol
 
   '!='        { Located $$ (Token (Op NotEqual    ) _)}
   '=='        { Located $$ (Token (Op Equal       ) _)}
-  '!==='      { Located $$ (Token (Op NotEqualFun ) _)}
+  '!=='       { Located $$ (Token (Op NotEqualFun ) _)}
   '==='       { Located $$ (Token (Op EqualFun    ) _)}
   '>'         { Located $$ (Token (Op GreaterThan ) _)}
   '<'         { Located $$ (Token (Op LessThan    ) _)}
@@ -156,7 +156,7 @@ import Paths_cryptol
 %left '||'
 %left '^'
 %left '&&'
-%nonassoc '==' '!=' '===' '!==='
+%nonassoc '==' '!=' '===' '!=='
 %nonassoc '<' '>' '<=' '>='
 %right '#'
 %left  '<<' '>>' '<<<' '>>>'
@@ -342,7 +342,7 @@ iexpr                            :: { Expr }
   | iexpr '==' iexpr                { binOp $1 (op ECEq          $2) $3 }
   | iexpr '!=' iexpr                { binOp $1 (op ECNotEq       $2) $3 }
   | iexpr '===' iexpr               { binOp $1 (op ECFunEq       $2) $3 }
-  | iexpr '!===' iexpr              { binOp $1 (op ECFunNotEq    $2) $3 }
+  | iexpr '!==' iexpr               { binOp $1 (op ECFunNotEq    $2) $3 }
   | iexpr '>' iexpr                 { binOp $1 (op ECGt          $2) $3 }
   | iexpr '<' iexpr                 { binOp $1 (op ECLt          $2) $3 }
   | iexpr '<=' iexpr                { binOp $1 (op ECLtEq        $2) $3 }
@@ -421,7 +421,7 @@ aexpr                          :: { Expr                                   }
   | '(' '=='   ')'                { at ($1,$3) $ ECon ECEq          }
   | '(' '!='   ')'                { at ($1,$3) $ ECon ECNotEq       }
   | '(' '==='  ')'                { at ($1,$3) $ ECon ECFunEq       }
-  | '(' '!===' ')'                { at ($1,$3) $ ECon ECFunNotEq    }
+  | '(' '!=='  ')'                { at ($1,$3) $ ECon ECFunNotEq    }
   | '(' '>'    ')'                { at ($1,$3) $ ECon ECGt          }
   | '(' '<'    ')'                { at ($1,$3) $ ECon ECLt          }
   | '(' '<='   ')'                { at ($1,$3) $ ECon ECLtEq        }
diff --git a/src/Cryptol/Prims/Syntax.hs b/src/Cryptol/Prims/Syntax.hs
index 48bde6ee..f011428d 100644
--- a/src/Cryptol/Prims/Syntax.hs
+++ b/src/Cryptol/Prims/Syntax.hs
@@ -159,7 +159,7 @@ instance PP ECon where
       ECEq          -> text "=="
       ECNotEq       -> text "!="
       ECFunEq       -> text "==="
-      ECFunNotEq    -> text "!==="
+      ECFunNotEq    -> text "!=="
       ECAnd         -> text "&&"
       ECOr          -> text "||"
       ECXor         -> text "^"
diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs
index dc370d51..0c866840 100644
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@@ -125,7 +125,7 @@ evalECon econ =
         cmpBinary cmpEq cmpEq SBV.true b x y
 
     ECFunNotEq    -> -- {a b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
-      -- (f !=== g) x = (f x != g x)
+      -- (f !== g) x = (f x != g x)
       tlam $ \_ ->
       tlam $ \b ->
       VFun $ \th1 -> return $