diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index d9f7bea495..1e949d2878 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -42,7 +42,10 @@ def «abbrev»         := parser! "abbrev " >> declId >> optDeclSig >> declVal
 def «def»            := parser! "def " >> declId >> optDeclSig >> declVal
 def «theorem»        := parser! "theorem " >> declId >> declSig >> declVal
 def «constant»       := parser! "constant " >> declId >> declSig >> optional declValSimple
-def «instance»       := parser! "instance " >> optional declId >> declSig >> declVal
+def «instance»       := parser!
+  (checkOutsideQuot >> "instance " >> optional declId >> declSig >> declVal)
+  <|>
+  (checkInsideQuot >> Term.attrKind >> "instance " >> optional declId >> declSig >> declVal)
 def «axiom»          := parser! "axiom " >> declId >> declSig
 def «example»        := parser! "example " >> declSig >> declVal
 def inferMod         := parser! atomic (symbol "{" >> "}")