diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml
index 0497d2bc4..b7c989e85 100644
--- a/lsp/lib/docs/proof_step.ml
+++ b/lsp/lib/docs/proof_step.ml
@@ -392,9 +392,7 @@ let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option =
            proof status between the modifications. *)
         let o =
           match o.fingerprint with
-          | None ->
-              (* `Tlapm_lib.Backend.Prep.prepare_obligation o` works too slow here. *)
-              Tlapm_lib.Backend.Fingerprints.write_fingerprint o
+          | None -> Tlapm_lib.Backend.Prep.prepare_obligation o
           | Some _ -> o
         in
         let o = Obl.of_parsed_obligation o in
diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml
index db9633b22..9bbf7cb94 100644
--- a/src/backend/fingerprints.ml
+++ b/src/backend/fingerprints.ml
@@ -446,14 +446,9 @@ and fp_sequent stack buf sq =
              spin stack cx;
              let v,r = Stack.pop stack in
              if !r then
-               (* Here `Expr.Levels.get_level e` was used instead of
-                  `if Expr.Constness.is_const e then 0 else 3`,
-                  but that introduces a dependency on having the levels
-                  assigned before calculating fingerprints. The former is
-                  slow and thus is problematic to use in LSP. *)
                bprintf buf "$Def(%d,%d)"
                        (match v with Identhypi i -> i | _ -> assert false)
-                       (if Expr.Constness.is_const e then 0 else 3)
+                       (Expr.Levels.get_level e)
           | Defn ({core = Bpragma (nm, _, _)}, _, Hidden, _) ->
              Stack.push stack (IdentBPragma nm.core, ref false);
              spin stack cx;