diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 718b114eae..7e3472afb7 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -112,3 +112,9 @@ macro_rules
   | `($a[$start : ])      => `(let a := $a; Array.toSubarray a $start a.size)
 
 end Array
+
+def Subarray.toArray (s : Subarray α) : Array α :=
+  Array.ofSubarray s
+
+instance : HAppend (Subarray α) (Subarray α) (Array α) where
+  hAppend x y := x.toArray ++ y.toArray
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index e6a9b769a8..a26c50c85e 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -518,6 +518,9 @@ def trim (s : String) : String :=
 def capitalize (s : String) :=
   s.set 0 <| s.get 0 |>.toUpper
 
+def decapitalize (s : String) :=
+  s.set 0 <| s.get 0 |>.toLower
+
 end String
 
 protected def Char.toString (c : Char) : String :=
diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 2b7cdbb430..306fc82ffe 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -186,6 +186,9 @@ structure InductiveVal extends ConstantVal where
   isReflexive : Bool
   isNested : Bool
 
+instance : Inhabited InductiveVal where
+  default := ⟨arbitrary, 0, 0, [], [], false, false, false, false⟩
+
 @[export lean_mk_inductive_val]
 def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat)
     (all ctors : List Name) (isRec isUnsafe isReflexive isNested : Bool) : InductiveVal := {
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 6624a080ac..f886704ce9 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -91,7 +91,7 @@ def openOnly         := parser! atomic (ident >> "(") >> many1 ident >> ")"
 def openSimple       := parser! many1 ident
 @[builtinCommandParser] def «open»    := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
 
-@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notSymbol "end" >> commandParser) >> "end"
+@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end")
 @[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
 @[builtinCommandParser] def «builtin_initialize» := parser! "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq