diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst
index 285036e682c..b7c85a308a7 100644
--- a/src/typechecker/FStar.TypeChecker.TcTerm.fst
+++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst
@@ -1754,7 +1754,8 @@ and tc_value env (e:term) : term
     let c, uc, f = tc_comp env c in
     let e = {U.arrow bs c with pos=top.pos} in
     (* checks the SMT pattern associated with this function is properly defined with regard to context *)
-    check_smt_pat env e bs c;
+    if not env.phase1 then
+      check_smt_pat env e bs c;
     (* taking the maximum of the universes of the computation and of all binders *)
     let u = S.U_max (uc::us) in
     (* create a universe of level u *)