diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
index 3b244d890a..3b80d8306d 100644
--- a/cryptol-saw-core/saw/Cryptol.sawcore
+++ b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -1073,6 +1073,12 @@ ecSMod n =
     (error (Stream Bool -> Stream Bool -> Stream Bool) "ecSMod: expected finite word")
     n;
 
+toSignedInteger : (n : Num) -> seq n Bool -> Integer;
+toSignedInteger n =
+  Num#rec (\ (n:Num) -> seq n Bool -> Integer)
+    sbvToInt
+    (error (Stream Bool -> Integer) "toSignedInteger: expected finite word")
+    n;
 
 -- Eq
 ecEq : (a : sort 0) -> PEq a -> a -> a -> Bool;
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 5e6a90a1e1..e4f5afa8c2 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -745,6 +745,8 @@ prelPrims =
   , ("%$",           flip scGlobalDef "Cryptol.ecSMod")        -- {n} (fin n, n>=1) => [n] -> [n] -> [n]
   , ("lg2",          flip scGlobalDef "Cryptol.ecLg2")         -- {n} (fin n) => [n] -> [n]
   , (">>$",          flip scGlobalDef "Cryptol.ecSShiftR")     -- {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
+  , ("toSignedInteger",
+                     flip scGlobalDef "Cryptol.toSignedInteger") -- {n} (fin n, n >= 1) => [n] -> Integer
 
     -- -- Rational primitives
   , ("ratio",        flip scGlobalDef "Cryptol.ecRatio")       -- Integer -> Integer -> Rational
diff --git a/deps/cryptol b/deps/cryptol
index 5a668a4594..cb240cdd31 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 5a668a4594e386a084f6f0ceb231c69946971a50
+Subproject commit cb240cdd31c864b298f181c0dac660e2f4e32aa5