diff --git a/meta_bindings.ml b/meta_bindings.ml
index fbc697d49ac836ef43c53944e739baec2db6bb0f..1317129fc60d14e2a12e691fa19a50d40971bfd2 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -172,7 +172,7 @@ let add_ghost_code flags =
       Ast.mark_as_changed ()
     end
 
-let search_global_var name = Globals.Vars.find_from_astinfo name VGlobal
+let search_global_var name = Globals.Vars.find_from_astinfo name Global
 
 (* Replace \binds by code adequately modifying _set and _size *)
 let make_static_modif_code name lvar =
diff --git a/meta_parse.ml b/meta_parse.ml
index 30a47f3c2badccce81b2cee0346ee34d73efc61d..d95011ce3029c8bd35b0d113d5932836c3ecdfec 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -139,14 +139,11 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
       let label = FormalLabel l in
       Logic_const.tat (e_t, label)
     | PLapp ("\\formal", _, [{lexpr_node = PLvar param}]) ->
-      let formals = Kernel_function.get_formals kf in
-      begin try
-        let vi = List.find (fun vi -> vi.vname = param) formals in
-        let lv = Cil.cvar_to_lvar vi in
-        Logic_const.tvar lv
-      with Not_found -> meta_ctxt.error loc "%s is not a formal in %a"
-                          param Kernel_function.pretty kf
-      end
+      (match Globals.Syntactic_search.find_in_scope param (Formal kf) with
+        | Some vi -> vi |> Cil.cvar_to_lvar |> Logic_const.tvar
+        | None ->
+          meta_ctxt.error loc "%s is not a formal in %a"
+            param Kernel_function.pretty kf)
     | PLapp ("\\bound", _, [bound]) ->
       Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
     | PLapp (app_name, _, [{lexpr_node = PLvar arg}])
@@ -256,7 +253,7 @@ let delay_prop tc name lexpr kf aslist =
     (* Tweak find_var so it can find things after link *)
     try tc.find_var var
     with Not_found -> try
-      let vi = Globals.Vars.find_from_astinfo var VGlobal in
+      let vi = Globals.Vars.find_from_astinfo var Global in
       Cil.cvar_to_lvar vi
     with Not_found ->
       let kf = Globals.Functions.find_by_name var in