diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 85e39e6918..853122f712 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -342,11 +342,12 @@ instance : Repr Int where
 def hexDigitRepr (n : Nat) : String :=
   String.singleton <| Nat.digitChar n
 
-def Char.quoteCore (c : Char) : String :=
+def Char.quoteCore (c : Char) (inString : Bool := false) : String :=
   if       c = '\n' then "\\n"
   else if  c = '\t' then "\\t"
   else if  c = '\\' then "\\\\"
   else if  c = '\"' then "\\\""
+  else if !inString && c = '\'' then "\\\'"
   else if  c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ smallCharToHex c
   else String.singleton c
 where
@@ -383,7 +384,7 @@ Examples:
 -/
 def String.quote (s : String) : String :=
   if s.isEmpty then "\"\""
-  else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
+  else s.foldl (fun s c => s ++ c.quoteCore (inString := true)) "\"" ++ "\""
 
 instance : Repr String where
   reprPrec s _ := s.quote
diff --git a/tests/lean/run/charQuote.lean b/tests/lean/run/charQuote.lean
new file mode 100644
index 0000000000..7c4c4b2d6c
--- /dev/null
+++ b/tests/lean/run/charQuote.lean
@@ -0,0 +1,7 @@
+-- This used to delaborate as `'''`, which is a parse error.
+
+/--
+info: '\''
+-/
+#guard_msgs in
+#eval '\''