diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index e96538e29..713ede488 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -317,6 +317,6 @@ expr parse_calc(parser & p) {
     buffer<expr> choices;
     for (auto const & s : steps)
         choices.push_back(step_proof(s));
-    return mk_choice(choices.size(), choices.data());
+    return p.save_pos(mk_choice(choices.size(), choices.data()), pos);
 }
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b3d380070..0f59206db 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -803,7 +803,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
         expr r = instantiate_rev(copy_with_new_pos(a, p), args.size(), args.data());
         cs.push_back(r);
     }
-    return mk_choice(cs.size(), cs.data());
+    return save_pos(mk_choice(cs.size(), cs.data()), p);
 }
 
 expr parser::parse_nud_notation() {