diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 0bba89ba93..ffb4e88435 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -69,9 +69,12 @@ instance [ToJson α] [ToJson β] : ToJson (α × β) where
 instance : FromJson Name where
   fromJson? j := do
     let s ← j.getStr?
-    let some n ← Syntax.decodeNameLit ("`" ++ s)
-      | throw s!"expected a `Name`, got '{j}'"
-    return n
+    if s == "[anonymous]" then
+      return Name.anonymous
+    else
+      let some n ← Syntax.decodeNameLit ("`" ++ s)
+        | throw s!"expected a `Name`, got '{j}'"
+      return n
 
 instance : ToJson Name where
   toJson n := toString n
diff --git a/tests/lean/679.lean b/tests/lean/679.lean
new file mode 100644
index 0000000000..d043ecbdbc
--- /dev/null
+++ b/tests/lean/679.lean
@@ -0,0 +1,8 @@
+import Lean
+open Lean
+
+def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
+  let json ← toJson x
+  fromJson? json
+
+#eval encodeDecode Name.anonymous
diff --git a/tests/lean/679.lean.expected.out b/tests/lean/679.lean.expected.out
new file mode 100644
index 0000000000..a7061a3e0d
--- /dev/null
+++ b/tests/lean/679.lean.expected.out
@@ -0,0 +1 @@
+Except.ok Lean.Name.anonymous