diff --git a/krmllib/dist/generic/FStar_FunctionalExtensionality.h b/krmllib/dist/generic/FStar_FunctionalExtensionality.h
index 91009383..d1904eb1 100644
--- a/krmllib/dist/generic/FStar_FunctionalExtensionality.h
+++ b/krmllib/dist/generic/FStar_FunctionalExtensionality.h
@@ -18,7 +18,7 @@ typedef void *FStar_FunctionalExtensionality_is_restricted;
 
 typedef void *FStar_FunctionalExtensionality_arrow_g;
 
-KRML_DEPRECATED("use arrow_g instead")
+KRML_DEPRECATED("Use arrow_g instead")
 
 typedef void *FStar_FunctionalExtensionality_efun_g;
 
diff --git a/lib/Helpers.ml b/lib/Helpers.ml
index 9a20aa3f..ab92adf6 100644
--- a/lib/Helpers.ml
+++ b/lib/Helpers.ml
@@ -267,24 +267,23 @@ let strengthen_array t e2 =
         size is non-constant, so I don't know what declaration to write"
         pexpr e2
 
+let pure_builtin_lids = ref [
+  [ "C"; "String" ], "get";
+  [ "C"; "Nullity" ], "op_Bang_Star";
+  [ "LowStar"; "BufferOps" ], "op_Bang_Star";
+  [ "Prims" ], "op_Minus";
+  [ "Lib"; "IntVector"; "Intrinsics" ], "vec128_smul64";
+  [ "Lib"; "IntVector"; "Intrinsics" ], "vec256_smul64";
+  [ "FStar"; "UInt32" ], "v";
+  [ "FStar"; "UInt128" ], "";
+]
+
 let is_readonly_builtin_lid lid =
-  let pure_builtin_lids = [
-    [ "C"; "String" ], "get";
-    [ "C"; "Nullity" ], "op_Bang_Star";
-    [ "LowStar"; "BufferOps" ], "op_Bang_Star";
-    [ "Prims" ], "op_Minus";
-    [ "Lib"; "IntVector"; "Intrinsics" ], "vec128_smul64";
-    [ "Lib"; "IntVector"; "Intrinsics" ], "vec256_smul64";
-    [ "FStar"; "UInt32" ], "v";
-    [ "FStar"; "UInt128" ], "";
-    [ "Eurydice" ], "vec_len";
-    [ "Eurydice" ], "vec_index";
-  ] in
   List.exists (fun lid' ->
     let lid = Idents.string_of_lident lid in
     let lid' = Idents.string_of_lident lid' in
     KString.starts_with lid lid'
-  ) pure_builtin_lids
+  ) !pure_builtin_lids
 
 class ['self] closed_term_visitor = object (_: 'self)
   inherit [_] reduce