diff --git a/src/Init/Lean/Util/PPGoal.lean b/src/Init/Lean/Util/PPGoal.lean
index bd1d058966..c264797706 100644
--- a/src/Init/Lean/Util/PPGoal.lean
+++ b/src/Init/Lean/Util/PPGoal.lean
@@ -21,7 +21,7 @@ match mctx.findDecl? mvarId with
     match ids, type? with
     | [], _        => fmt
     | _, none      => fmt
-    | _, some type => fmt ++ (Format.joinSep ids " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
+    | _, some type => fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
   let (varNames, type?, fmt) := mvarDecl.lctx.foldl
     (fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) =>
        let (varNames, prevType?, fmt) := acc;