diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
index 13be0bb46a9..4ed38d3be42 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
@@ -5805,8 +5805,10 @@ and (do_check :
                                     match uu___8 with
                                     | (g_as_x, as_x2, returns_ty1) ->
                                         let uu___9 =
-                                          check "return type" g_as_x
-                                            returns_ty1 in
+                                          let uu___10 =
+                                            check "return type" g_as_x
+                                              returns_ty1 in
+                                          with_binders [as_x2] [x1] uu___10 in
                                         (fun ctx02 ->
                                            let uu___10 = uu___9 ctx02 in
                                            match uu___10 with
diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst
index e78df451820..cbd0040593b 100644
--- a/src/typechecker/FStar.TypeChecker.Core.fst
+++ b/src/typechecker/FStar.TypeChecker.Core.fst
@@ -1480,7 +1480,8 @@ and do_check (g:env) (e:term)
     let! u_sc = with_context "universe_of" (Some (CtxTerm t_sc)) (fun _ -> universe_of g t_sc) in
     let as_x = {as_x with binder_bv = { as_x.binder_bv with sort = t_sc } } in
     let g_as_x, as_x, returns_ty = open_term g as_x returns_ty in
-    let! _eff_t, returns_ty_t = check "return type" g_as_x returns_ty in
+    let! _eff_t, returns_ty_t =
+      with_binders [as_x] [u_sc] (check "return type" g_as_x returns_ty) in
     let! _u_ty = is_type g_as_x returns_ty_t in
     let rec check_branches (path_condition: S.term)
                            (branches: list S.branch)