diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 516a6b801459774ca3bb8a74661a75deefa645a3..69e3a0ea22a775b3f89247091212618447289c0e 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -878,14 +878,18 @@ struct
         | LFUN phi -> e_fun phi [] ~result:(Lang.tau_of_ltype x.lv_type)
       in Cvalues.plain x.lv_type v
     with Not_found ->
-      Wp_parameters.fatal "Unbound logic variable '%a'"
-        Printer.pp_logic_var x
+      if Logic_env.is_logic_function x.lv_name then
+        Warning.error "Lambda-functions not yet implemented (at '%s')"
+          x.lv_name
+      else
+        Wp_parameters.fatal "Name '%a' has no definition in term"
+          Printer.pp_logic_var x
 
   let logic_info env f =
     try
       match Logic_var.Map.find f.l_var_info env.vars with
       | Vexp p -> Some (F.p_bool p)
-      | _ -> Wp_parameters.fatal "Logic variable '%a' is not a predicate"
+      | _ -> Wp_parameters.fatal "Variable '%a' is not a predicate"
                Logic_info.pretty f
     with Not_found -> None