diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
index 90eec7b5514..e289b3f75e6 100644
--- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
@@ -3510,27 +3510,18 @@ and (desugar_term_maybe_top :
                           mk (FStar_Syntax_Syntax.Tm_uinst (head, universes)) in
                         (uu___7, aq)) in
              aux [] top
-         | FStar_Parser_AST.App uu___2 ->
-             let rec aux args aqs e =
-               let uu___3 =
-                 let uu___4 = unparen e in uu___4.FStar_Parser_AST.tm in
-               match uu___3 with
-               | FStar_Parser_AST.App (e1, t, imp) when
-                   imp <> FStar_Parser_AST.UnivApp ->
-                   let uu___4 = desugar_term_aq env t in
-                   (match uu___4 with
-                    | (t1, aq) ->
-                        let arg = arg_withimp_t imp t1 in
-                        aux (arg :: args) (aq :: aqs) e1)
-               | uu___4 ->
-                   let uu___5 = desugar_term_aq env e in
-                   (match uu___5 with
-                    | (head, aq) ->
-                        let uu___6 =
-                          FStar_Syntax_Syntax.extend_app_n head args
-                            top.FStar_Parser_AST.range in
-                        (uu___6, (join_aqs (aq :: aqs)))) in
-             aux [] [] top
+         | FStar_Parser_AST.App (e, t, imp) ->
+             let uu___2 = desugar_term_aq env e in
+             (match uu___2 with
+              | (head, aq1) ->
+                  let uu___3 = desugar_term_aq env t in
+                  (match uu___3 with
+                   | (t1, aq2) ->
+                       let arg = arg_withimp_t imp t1 in
+                       let uu___4 =
+                         FStar_Syntax_Syntax.extend_app head arg
+                           top.FStar_Parser_AST.range in
+                       (uu___4, (FStar_Compiler_List.op_At aq1 aq2))))
          | FStar_Parser_AST.Bind (x, t1, t2) ->
              let xpat =
                let uu___2 = FStar_Ident.range_of_id x in
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index 30ed68488f3..3eea02ba793 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -1512,17 +1512,11 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an
                 mk (Tm_uinst(head, universes)), aq
        in aux [] top
 
-    | App _ ->
-      let rec aux args aqs e = match (unparen e).tm with
-        | App(e, t, imp) when imp <> UnivApp ->
-          let t, aq = desugar_term_aq env t in
-          let arg = arg_withimp_t imp t in
-          aux (arg::args) (aq::aqs) e
-        | _ ->
-          let head, aq = desugar_term_aq env e in
-          S.extend_app_n head args top.range, join_aqs (aq::aqs)
-      in
-      aux [] [] top
+    | App (e, t, imp) ->
+      let head, aq1 = desugar_term_aq env e in
+      let t, aq2 = desugar_term_aq env t in
+      let arg = arg_withimp_t imp t in
+      S.extend_app head arg top.range, aq1@aq2
 
     | Bind(x, t1, t2) ->
       let xpat = AST.mk_pattern (AST.PatVar(x, None, [])) (range_of_id x) in
diff --git a/tests/error-messages/DesugarOrder.fst b/tests/error-messages/DesugarOrder.fst
new file mode 100644
index 00000000000..8cf057a17e6
--- /dev/null
+++ b/tests/error-messages/DesugarOrder.fst
@@ -0,0 +1,7 @@
+module DesugarOrder
+
+(* Report 'a' as not found, instead of 'c'. It's clearer
+to report errors in textual order. Ideally, we could report all of them
+at once (also in order). *)
+[@@expect_failure]
+let _ = (+) a b c
diff --git a/tests/error-messages/DesugarOrder.fst.expected b/tests/error-messages/DesugarOrder.fst.expected
new file mode 100644
index 00000000000..098a5082621
--- /dev/null
+++ b/tests/error-messages/DesugarOrder.fst.expected
@@ -0,0 +1,7 @@
+>> Got issues: [
+* Error 72 at DesugarOrder.fst(7,12-7,13):
+  - Identifier not found: [a]
+
+>>]
+Verified module: DesugarOrder
+All verification conditions discharged successfully
diff --git a/tests/error-messages/DesugarOrder.fst.json_expected b/tests/error-messages/DesugarOrder.fst.json_expected
new file mode 100644
index 00000000000..297c300a971
--- /dev/null
+++ b/tests/error-messages/DesugarOrder.fst.json_expected
@@ -0,0 +1,5 @@
+>> Got issues: [
+{"msg":["Identifier not found: [a]"],"level":"Error","range":{"def":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}},"use":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}}},"number":72,"ctx":["While desugaring module DesugarOrder"]}
+>>]
+Verified module: DesugarOrder
+All verification conditions discharged successfully