diff --git a/tests/lean/interactive/coe.input.expected.out b/tests/lean/interactive/coe.input.expected.out
index 23514d74c..8002a75ae 100644
--- a/tests/lean/interactive/coe.input.expected.out
+++ b/tests/lean/interactive/coe.input.expected.out
@@ -5,7 +5,7 @@
 decidable (a = b)
 -- ACK
 -- SYNTH|5|16
-int.has_decidable_eq a b
+has_decidable_eq a b
 -- ACK
 -- SYMBOL|5|16
 _