diff --git a/src/lean.ml b/src/lean.ml
index 9bad8c6..1372099 100644
--- a/src/lean.ml
+++ b/src/lean.ml
@@ -898,7 +898,7 @@ and declare_def n { ty; body; univs; height } i =
   in
   let () =
     let c = match ref with ConstRef c -> c | _ -> assert false in
-    Global.set_strategy (ConstKey c) (Level (-height))
+    Global.set_strategy (Evaluable.EvalConstRef c) (Level (-height))
   in
   let inst = { ref; algs } in
   let () = add_declared n i inst in