diff --git a/lib/Builtin.ml b/lib/Builtin.ml
index 613397a6..3f8fb229 100644
--- a/lib/Builtin.ml
+++ b/lib/Builtin.ml
@@ -437,8 +437,8 @@ let prepare files =
      F* PR: References to module C can now occur even when the module is not in the scope.
      If so, we add the definition that is needed as a builtin, since it will be rewritten
      during C code generation *)
-  if List.mem_assoc "C" files then [] else [c_deref] @
-  if List.mem_assoc "LowStar_Ignore" files then [] else [lowstar_ignore] @
+  (if List.mem_assoc "C" files then [] else [c_deref]) @
+  (if List.mem_assoc "LowStar_Ignore" files then [] else [lowstar_ignore]) @
   []
 
 let make_libraries files =
diff --git a/lib/Checker.ml b/lib/Checker.ml
index 11658951..35cf0afb 100644
--- a/lib/Checker.ml
+++ b/lib/Checker.ml
@@ -536,9 +536,9 @@ and infer' env e =
   let infer_app t es =
     let t_ret, t_args = flatten_arrow t in
     if List.length t_args = 0 then
-      checker_error env "This is not a function:\n%a" pexpr e;
+      checker_error env "This is not a function type:\n%a a.k.a. %s\n" ptyp t (show_typ t);
     if List.length es > List.length t_args then
-      checker_error env "Too many arguments for application:\n%a" pexpr e;
+      checker_error env "Too many arguments for application:\n%a" pexprs es;
     let t_args, t_remaining_args = KList.split (List.length es) t_args in
     ignore (List.map2 (check_or_infer env) t_args es);
     fold_arrow t_remaining_args t_ret