diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml
index 3b98244c239..5f9344d37d6 100644
--- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml
+++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml
@@ -1953,7 +1953,7 @@ let rec (translate_type_without_decay' :
       | FStar_Extraction_ML_Syntax.MLTY_Named ([], ("FStar"::m::[], "t'"))
           when is_machine_int m ->
           let uu___ = FStar_Compiler_Util.must (mk_width m) in TInt uu___
-      | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when
+      | FStar_Extraction_ML_Syntax.MLTY_Named ([], p) when
           let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in
           uu___ = "FStar.Monotonic.HyperStack.mem" -> TUnit
       | FStar_Extraction_ML_Syntax.MLTY_Named (uu___::arg::uu___1::[], p)
@@ -4117,7 +4117,7 @@ let (translate :
                        "Unable to translate module: %s because:\n  %s\n"
                        m_name uu___3);
                     FStar_Pervasives_Native.None)) modules
-let (uu___2021 : unit) =
+let (uu___2020 : unit) =
   register_post_translate_type_without_decay translate_type_without_decay';
   register_post_translate_type translate_type';
   register_post_translate_type_decl translate_type_decl';
diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst
index 24837b3010a..5f10cf857ea 100644
--- a/src/extraction/FStar.Extraction.Krml.fst
+++ b/src/extraction/FStar.Extraction.Krml.fst
@@ -660,7 +660,7 @@ let rec translate_type_without_decay' env t: typ =
       TInt (must (mk_width m))
   | MLTY_Named ([], ([ "FStar"; m ], "t'")) when is_machine_int m ->
       TInt (must (mk_width m))
-  | MLTY_Named ([arg], p) when (Syntax.string_of_mlpath p = "FStar.Monotonic.HyperStack.mem") ->
+  | MLTY_Named ([], p) when (Syntax.string_of_mlpath p = "FStar.Monotonic.HyperStack.mem") ->
       TUnit
   
   | MLTY_Named ([_; arg; _], p) when