diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index 4ba9d484..06669de3 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -53,6 +53,9 @@ var leanHighlightRules = function() {
           "universes", "using", "variable", "variables", "with"].join("|")
     );
 
+    var nameProviders = (
+        ["inductive", "structure", "record", "theorem", "axiom",
+         "axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
     );
 
     var storageType = (
@@ -109,6 +112,8 @@ var leanHighlightRules = function() {
                     {defaultToken: "string"}
                 ]
             }, {
+                token : "keyword.control", regex : nameProviders, next : [
+                    {token : "variable.language", regex : identifierRe, next : "start"} ]
             }, {
                 token : "constant.numeric", // hex
                 regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"