diff --git a/Game/Tactic/Xyzzy.lean b/Game/Tactic/Xyzzy.lean
index 927c343..01f0d49 100644
--- a/Game/Tactic/Xyzzy.lean
+++ b/Game/Tactic/Xyzzy.lean
@@ -3,11 +3,11 @@ import Lean
 universe u
 
 @[never_extract]
-axiom iGiveUpAx (α : Sort u) (synthetic := false) : α
+axiom xyzzyAxiom (α : Sort u) (synthetic := false) : α
 
 /--
 `xyzzy` is an ancient magic word, believed to be the root of the
 modern word `sorry`. The game won't complain - or notice - if you
 prove anything with `xyzzy`.
 -/
-macro "xyzzy" : tactic => `(tactic| exact @iGiveUpAx _ false)
+macro "xyzzy" : tactic => `(tactic| exact @xyzzyAxiom _ false)