diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index 33bd093096..b836dfc278 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -31,11 +31,16 @@ ppParams = \case
     ps <- mapM ppCode params
     return $ Just $ parens (hsep (punctuate comma ps))
 
-ppJudocComment :: Maybe Text -> Sem r (Doc Ann)
-ppJudocComment = \case
+ppTextComment :: Maybe Text -> Sem r (Doc Ann)
+ppTextComment = \case
   Nothing -> return ""
   Just c -> return $ annotate AnnComment "text \\<open>" <> line <> annotate AnnComment (pretty c) <> line <> annotate AnnComment "\\<close>" <> line
 
+ppComment :: Maybe Text -> Sem r (Doc Ann)
+ppComment = \case
+  Nothing -> return ""
+  Just c -> return $ annotate AnnComment "(* " <> annotate AnnComment (pretty c) <> annotate AnnComment " *)" <> line
+
 instance PrettyCode Name where
   ppCode = return . prettyName False
 
@@ -195,7 +200,7 @@ instance PrettyCode Statement where
 
 instance PrettyCode Definition where
   ppCode Definition {..} = do
-    comment <- ppJudocComment _definitionComment
+    comment <- ppTextComment _definitionComment
     n <- ppCode _definitionName
     ty <- ppCodeQuoted _definitionType
     body <- ppCode _definitionBody
@@ -203,7 +208,7 @@ instance PrettyCode Definition where
 
 instance PrettyCode Function where
   ppCode Function {..} = do
-    comment <- ppJudocComment _functionComment
+    comment <- ppTextComment _functionComment
     n <- ppCode _functionName
     ty <- ppCodeQuoted _functionType
     cls <- mapM ppCode _functionClauses
@@ -218,14 +223,14 @@ instance PrettyCode Clause where
 
 instance PrettyCode Synonym where
   ppCode Synonym {..} = do
-    comment <- ppJudocComment _synonymComment
+    comment <- ppTextComment _synonymComment
     n <- ppCode _synonymName
     ty <- ppCodeQuoted _synonymType
     return $ comment <> kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
 
 instance PrettyCode Datatype where
   ppCode Datatype {..} = do
-    comment <- ppJudocComment _datatypeComment
+    comment <- ppTextComment _datatypeComment
     n <- ppCode _datatypeName
     params <- ppParams _datatypeParams
     ctrs <- mapM ppCode _datatypeConstructors
@@ -233,14 +238,14 @@ instance PrettyCode Datatype where
 
 instance PrettyCode Constructor where
   ppCode Constructor {..} = do
-    comment <- ppJudocComment _constructorComment
+    comment <- ppComment _constructorComment
     n <- ppCode _constructorName
     tys <- mapM ppCodeQuoted _constructorArgTypes
     return $ comment <> hsep (n : tys)
 
 instance PrettyCode Record where
   ppCode Record {..} = do
-    comment <- ppJudocComment _recordComment
+    comment <- ppTextComment _recordComment
     n <- ppCode _recordName
     params <- ppParams _recordParams
     fields <- mapM ppCode _recordFields
@@ -248,7 +253,7 @@ instance PrettyCode Record where
 
 instance PrettyCode RecordField where
   ppCode RecordField {..} = do
-    comment <- ppJudocComment _recordFieldComment
+    comment <- ppComment _recordFieldComment
     n <- ppCode _recordFieldName
     ty <- ppCodeQuoted _recordFieldType
     return $ comment <> n <+> "::" <+> ty
diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
index 1743ae7cec..2e865deda5 100644
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@@ -89,7 +89,11 @@ funkcja (n : Nat) : Nat :=
   in plusOne n + nat1 + nat2;
 
 --- An Either' type
-type Either' A B := Left' A | Right' B;
+type Either' A B :=
+  --- Left constructor
+  Left' A
+| --- Right constructor
+  Right' B;
 
 -- Records
 
diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
index e0bc3df479..3c846b64c4 100644
--- a/tests/positive/Isabelle/isabelle/Program.thy
+++ b/tests/positive/Isabelle/isabelle/Program.thy
@@ -105,7 +105,9 @@ text \<open>
 An Either' type
 \<close>
 datatype ('A, 'B) Either'
-  = Left' 'A |
+  = (* Left constructor *)
+    Left' 'A |
+    (* Right constructor *)
     Right' 'B
 
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where