diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
index b77139a0f79..1fc4232fece 100644
--- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
+++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -3744,8 +3744,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         } else {
           error := Some("Unrecognized external file " + externalFile + ". External file must be *.rs files");
         }
-        var externMod := R.ExternMod(externalMod);
-        s := s + externMod.ToString("") + "\n";
+        if rootType.RootCrate? {
+          var externMod := R.ExternMod(externalMod);
+          s := s + externMod.ToString("") + "\n";
+        }
         externUseDecls := externUseDecls + [
           R.UseDecl(R.Use(R.PUB, R.crate.MSel(externalMod).MSel("*")))
         ];
diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
index 9158c6ca83b..4482140deb5 100644
--- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
+++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
@@ -6679,9 +6679,11 @@ public RAST._IExpr Error(Dafny.ISequence<Dafny.Rune> message, RAST._IExpr defaul
         } else {
           (this).error = Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Unrecognized external file "), _2_externalFile), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(". External file must be *.rs files")));
         }
-        RAST._IMod _4_externMod;
-        _4_externMod = RAST.Mod.create_ExternMod(_3_externalMod);
-        s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_4_externMod)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
+        if (((this).rootType).is_RootCrate) {
+          RAST._IMod _4_externMod;
+          _4_externMod = RAST.Mod.create_ExternMod(_3_externalMod);
+          s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_4_externMod)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
+        }
         _0_externUseDecls = Dafny.Sequence<RAST._IModDecl>.Concat(_0_externUseDecls, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), ((RAST.__default.crate).MSel(_3_externalMod)).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("*"))))));
       }
       if (!(_0_externUseDecls).Equals(Dafny.Sequence<RAST._IModDecl>.FromElements())) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy
index e4facc514b9..c55fc26cb3f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy
@@ -1,12 +1,16 @@
-// RUN: %baredafny translate rs --rust-module-name additional_module "%s"
+// RUN: %baredafny translate rs --rust-module-name additional_module "%S/more_dafny_extern.rs" "%s"
 // RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/additional_module.rs"
+// RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/more_dafny_extern.rs"
 // RUN: %mv "%S/more_dafny-rust/src/more_dafny.rs" "%S/project_depending_on_dafny/src/additional_module.rs"
+// RUN: %mv "%S/more_dafny-rust/src/more_dafny_extern.rs" "%S/project_depending_on_dafny/src/more_dafny_extern.rs"
 // RUN: "%S/project_depending_on_dafny/cargo" run > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module SubModule {
+  function {:axiom} {:extern "extern_dafny", "eight"} Eight(): (r: bv16) ensures r == 8
+
   function reverse(input: bv16): bv16 {
-    ((input & 0xFF) << 8) | ((input & 0xFF00) >> 8)
+    ((input & 0xFF) << Eight()) | ((input & 0xFF00) >> Eight())
   }
 }
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny_extern.rs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny_extern.rs
new file mode 100644
index 00000000000..59348bf4c2a
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny_extern.rs
@@ -0,0 +1,5 @@
+pub mod extern_dafny {
+  pub fn eight() -> u16 {
+    8
+  }
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore
index bc950be1152..d149df7bd20 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore
@@ -1,2 +1,3 @@
 src/additional_module.rs
+src/more_dafny_extern.rs
 target/
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs
index 3dc44c6beae..ddcab2f93c8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs
@@ -1,4 +1,5 @@
 pub mod additional_module;
+pub mod more_dafny_extern;
 
 fn main() {
   let x = additional_module::_module::_default::reverse(10);