diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2af25e26a1..03194d5f4a 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -70,7 +70,16 @@ def sufficesDecl := optIdent >> termParser >> (fromTerm <|> byTactic)
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
 def structInstField  := ppGroup $ parser! structInstLVal >> " := " >> termParser
-@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
+@[builtinTermParser] def structInst := parser!
+  (checkInsideQuot >>
+  "{" >> ppHardSpace >> optional (atomic (termParser >> " with "))
+  >> manyIndent (group (structInstField >> optional ", "))
+  >> optional ".."
+  >> optional (" : " >> termParser) >> " }")
+  <|>
+  (checkOutsideQuot >>
+    "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }")
+
 def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
 @[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec