From 5830da9e2d33d0ce309a4be2f0db70f2f5722435 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Oct 2014 14:44:59 -0700 Subject: [PATCH] fix(frontends/lean/tokens): typo --- src/frontends/lean/tokens.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index dda113bf6..4e191063e 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -321,7 +321,7 @@ name const & get_end_tk() { return *g_end; } name const & get_definition_tk() { return *g_definition; } name const & get_theorem_tk() { return *g_theorem; } name const & get_axiom_tk() { return *g_axiom; } -name const & get_axioms_tk() { return *g_axiom; } +name const & get_axioms_tk() { return *g_axioms; } name const & get_variable_tk() { return *g_variable; } name const & get_variables_tk() { return *g_variables; } name const & get_opaque_tk() { return *g_opaque; }