diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index f5d524f650..3b3b255bd4 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -80,7 +80,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
   where
     toIsabelleTheoryName :: Text -> Text
     toIsabelleTheoryName name =
-      Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
+      quote . Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
 
     isTypeDef :: Statement -> Bool
     isTypeDef = \case
@@ -1219,8 +1219,25 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
     quote :: Text -> Text
-    quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+    quote txt0
+      | Text.elem '.' txt0 = moduleName' <> "." <> idenName'
+      | otherwise = quote'' txt0
       where
+        (moduleName, idenName) = Text.breakOnEnd "." txt0
+        moduleName' = toIsabelleTheoryName (removeLastDot moduleName)
+        idenName' = quote'' idenName
+
+        removeLastDot :: Text -> Text
+        removeLastDot txt
+          | Text.last txt == '.' = Text.init txt
+          | otherwise = txt
+
+        quote'' :: Text -> Text
+        quote'' =
+          quote'
+            . Text.filter isLatin1
+            . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+
         quote' :: Text -> Text
         quote' txt
           | HashSet.member txt reservedNames = quote' (prime txt)
diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs
index d464a50115..8c88ea85e1 100644
--- a/src/Juvix/Parser/Error.hs
+++ b/src/Juvix/Parser/Error.hs
@@ -177,7 +177,7 @@ instance ToGenericError StdinOrFileError where
   genericError StdinOrFileError =
     return
       GenericError
-        { _genericErrorLoc = singletonInterval (mkInitialLoc formatStdinPath),
+        { _genericErrorLoc = singletonInterval (mkInitialLoc noFile),
           _genericErrorMessage = prettyError "Neither JUVIX_FILE_OR_PROJECT nor --stdin option is chosen",
           _genericErrorIntervals = []
         }
diff --git a/tests/positive/Isabelle/M/Main.juvix b/tests/positive/Isabelle/M/Main.juvix
new file mode 100644
index 0000000000..b8e8ac4086
--- /dev/null
+++ b/tests/positive/Isabelle/M/Main.juvix
@@ -0,0 +1,6 @@
+module M.Main;
+
+import Stdlib.Prelude open;
+import M.N open;
+
+f (a : Nat) : Nat := g a;
diff --git a/tests/positive/Isabelle/M/N.juvix b/tests/positive/Isabelle/M/N.juvix
new file mode 100644
index 0000000000..092cfc76c8
--- /dev/null
+++ b/tests/positive/Isabelle/M/N.juvix
@@ -0,0 +1,5 @@
+module M.N;
+
+import Stdlib.Prelude open;
+
+g (a : Nat) : Nat := a + 1;
diff --git a/tests/positive/Isabelle/N.juvix b/tests/positive/Isabelle/N.juvix
new file mode 100644
index 0000000000..db6ae1ffe4
--- /dev/null
+++ b/tests/positive/Isabelle/N.juvix
@@ -0,0 +1,5 @@
+module N;
+
+import Stdlib.Prelude open;
+
+g (a : Nat) : Nat := a * 2;
diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
index 7e7db6324b..217bae8939 100644
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@@ -1,6 +1,9 @@
 module Program;
 
 import Stdlib.Prelude open;
+import N;
+import M.N;
+import M.Main as Main;
 
 id0 : Nat -> Nat := id;
 
@@ -23,7 +26,7 @@ f (x y : Nat) : Nat -> Nat
 
 g (x y : Nat) : Bool :=
   if
-    | x == y := false
+    | x == f x (N.g y) (M.N.g (Main.f y)) := false
     | else := true;
 
 inc (x : Nat) : Nat := suc x;
diff --git a/tests/positive/Isabelle/isabelle/M_Main.thy b/tests/positive/Isabelle/isabelle/M_Main.thy
new file mode 100644
index 0000000000..2a6d0c82a8
--- /dev/null
+++ b/tests/positive/Isabelle/isabelle/M_Main.thy
@@ -0,0 +1,9 @@
+theory M_Main
+imports Main
+        M_N
+begin
+
+fun f :: "nat \<Rightarrow> nat" where
+  "f a = (g a)"
+
+end
diff --git a/tests/positive/Isabelle/isabelle/M_N.thy b/tests/positive/Isabelle/isabelle/M_N.thy
new file mode 100644
index 0000000000..76d2300fbd
--- /dev/null
+++ b/tests/positive/Isabelle/isabelle/M_N.thy
@@ -0,0 +1,8 @@
+theory M_N
+imports Main
+begin
+
+fun g :: "nat \<Rightarrow> nat" where
+  "g a = (a + 1)"
+
+end
diff --git a/tests/positive/Isabelle/isabelle/N.thy b/tests/positive/Isabelle/isabelle/N.thy
new file mode 100644
index 0000000000..1e706f594a
--- /dev/null
+++ b/tests/positive/Isabelle/isabelle/N.thy
@@ -0,0 +1,8 @@
+theory N
+imports Main
+begin
+
+fun g :: "nat \<Rightarrow> nat" where
+  "g a = (a * 2)"
+
+end
diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
index 2d7324f431..fec5012e10 100644
--- a/tests/positive/Isabelle/isabelle/Program.thy
+++ b/tests/positive/Isabelle/isabelle/Program.thy
@@ -1,5 +1,8 @@
 theory Program
 imports Main
+        N
+        M_N
+        M_Main
 begin
 
 definition id0 :: "nat \<Rightarrow> nat" where
@@ -25,7 +28,7 @@ fun f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "f x y z = ((z + 1) * x + y)"
 
 fun g :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-  "g x y = (if x = y then False else True)"
+  "g x y = (if x = f x (N.g y) (M_N.g (M_Main.f y)) then False else True)"
 
 fun inc :: "nat \<Rightarrow> nat" where
   "inc x = (Suc x)"