diff --git a/demo/Demo.lean b/demo/Demo.lean
index 8a9e226..2e70ebc 100644
--- a/demo/Demo.lean
+++ b/demo/Demo.lean
@@ -22,3 +22,9 @@ theorem test (n : Nat) : n * 1 = n := by
     rw [← ih]
     simp
 %end
+
+%example proofWithInstance
+-- Test that proof states containing daggered names can round-trip
+def test2 [ToString α] (x : α) : Decidable (toString x = "") := by
+  constructor; sorry
+%end
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
index 20a6c23..3dac222 100644
--- a/src/examples/SubVerso/Examples.lean
+++ b/src/examples/SubVerso/Examples.lean
@@ -232,12 +232,3 @@ def wxyz (n : Nat) := 1 + 3 + n
 #check wxyz
 def xyz (n : Nat) := 1 + %ex{test2}{3 + n}
 %end
-
-
--- %example test
--- #eval 5
--- %end
-
--- %dump test
--- %dump test3.test2
--- %dump test3
diff --git a/src/highlighting/SubVerso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
index 47d057e..fb38b8f 100644
--- a/src/highlighting/SubVerso/Highlighting/Highlighted.lean
+++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
@@ -7,6 +7,30 @@ namespace SubVerso.Highlighting
 deriving instance Repr for Std.Format.FlattenBehavior
 deriving instance Repr for Std.Format
 
+-- Workaround for the fact that the default From/ToJson instances for Name
+-- don't always round-trip
+
+private def altNameJson (n : Name) : Json := Json.arr (splitName #[] n)
+where
+  splitName acc
+    | .anonymous => acc
+    | .num x n => splitName acc x |>.push n
+    | .str x s => splitName acc x |>.push s
+
+private def altNameUnJson (json : Json) : Except String Name := do
+  let arr ← json.getArr?
+  let mut n := .anonymous
+  for v in arr do
+    match v with
+    | (s : String) => n := n.str s
+    | (i : Nat) => n := n.num i
+    | other => .error s!"Expected a string or number as a name component, got '{other}'"
+  pure n
+
+private local instance : ToJson Name := ⟨altNameJson⟩
+private local instance : FromJson Name := ⟨altNameUnJson⟩
+
+
 inductive Token.Kind where
   | /-- `occurrence` is a unique identifier that unites the various keyword tokens from a given production -/
     keyword (name : Option Name) (occurrence : Option String) (docs : Option String)