diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 4e41c86c77bf..4779992cb04d 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -977,7 +977,7 @@ See the Chapter "Quantifiers and Equality" in the manual
 "Theorem Proving in Lean" for additional information.
 -/
 @[builtin_term_parser] def subst := trailing_parser:75
-  " ▸ " >> sepBy1 (termParser 75) " ▸ "
+  " ▸ " >> termParser 75
 
 def bracketedBinderF := bracketedBinder  -- no default arg
 instance : Coe (TSyntax ``bracketedBinderF) (TSyntax ``bracketedBinder) where coe s := ⟨s⟩
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 3baec9ac0fdd..d96a46b866db 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,6 +1,6 @@
 #include "util/options.h"
 
-// [ ] Check box to force CI to test stage 2 and run update-stage0 on PR merge
+// [x] Check box to force CI to test stage 2 and run update-stage0 on PR merge
 // (any other change to this file will do the same; ALL changes should be made to the stage0/ copy)
 
 namespace lean {