diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java
index 41325fb1a..1cbc659cf 100644
--- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java
+++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java
@@ -12,7 +12,7 @@
 import software.amazon.cryptography.primitives.internaldafny.types.Error;
 import software.amazon.cryptography.primitives.model.AwsCryptographicPrimitivesError;
 
-public class HMac extends _ExternBase_HMac {
+public class HMac extends _ExternBase___default {
 
   private String algorithm;
   private Mac hmac;
diff --git a/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy b/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy
index 4d8f4b5e6..0e0c4e24f 100644
--- a/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy
+++ b/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy
@@ -63,13 +63,7 @@ module {:options "-functionSyntax:4"} {:extern "HMAC"} HMAC {
     // since their calling pattern is different between different versions of Dafny
     // (i.e. after 4.2, explicit type descriptors are required).
 
-    static function CreateHMacSuccess(hmac: HMac): Result<HMac, Types.Error> {
-      Success(hmac)
-    }
 
-    static function CreateHMacFailure(error: Types.Error): Result<HMac, Types.Error> {
-      Failure(error)
-    }
   }
 
   // HMAC Digest is safe to make a Dafny function
@@ -78,11 +72,19 @@ module {:options "-functionSyntax:4"} {:extern "HMAC"} HMAC {
     : ( output: Result<seq<uint8>, Types.Error> )
     ensures output.Success? ==> |output.value| == HashDigest.Length(input.digestAlgorithm)
 
-  // The next two functions are for the benefit of the extern implementation to call,
+  // The following functions are for the benefit of the extern implementation to call,
   // avoiding direct references to generic datatype constructors
   // since their calling pattern is different between different versions of Dafny
   // (i.e. after 4.2, explicit type descriptors are required).
 
+  function CreateHMacSuccess(hmac: HMac): Result<HMac, Types.Error> {
+    Success(hmac)
+  }
+
+  function CreateHMacFailure(error: Types.Error): Result<HMac, Types.Error> {
+    Failure(error)
+  }
+
   function CreateDigestSuccess(bytes: seq<uint8>): Result<seq<uint8>, Types.Error> {
     Success(bytes)
   }