diff --git a/comparator/Main.lean b/comparator/Main.lean
index 3fe7c5411..284f7a3c7 100644
--- a/comparator/Main.lean
+++ b/comparator/Main.lean
@@ -5,7 +5,6 @@ Authors: Henrik Böving
 -/
 import Lean
 import Comparator
-import Lean4Checker.Replay
 import Export.Parse
 
 namespace Comparator
@@ -198,7 +197,7 @@ def runKernel (solution : Export.ExportedEnv) : M Unit := do
   -- Lean's kernel interprets just the addition of `Quot as adding all of these so adding them
   -- multiple times leads to errors.
   constMap := constMap.erase `Quot.mk |>.erase `Quot.lift |>.erase `Quot.ind
-  discard <| env.replay' constMap
+  discard <| env.replay constMap
   IO.println "Lean default kernel accepts the solution"
 
 def primitiveTargets : M (Array Lean.Name) := do
diff --git a/comparator/lake-manifest.json b/comparator/lake-manifest.json
index 3cbb6ab9e..4f014bf4e 100644
--- a/comparator/lake-manifest.json
+++ b/comparator/lake-manifest.json
@@ -10,16 +10,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4checker",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "b7398199245524275543dec6113229c9bb4902e5",
-   "name": "Lean4Checker",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "b7398199245524275543dec6113229c9bb4902e5",
-   "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "Comparator",
  "lakeDir": ".lake",
diff --git a/comparator/lakefile.toml b/comparator/lakefile.toml
index 1865ae821..8b55152f7 100644
--- a/comparator/lakefile.toml
+++ b/comparator/lakefile.toml
@@ -9,11 +9,6 @@ name = "Comparator"
 name = "comparator"
 root = "Main"
 
-[[require]]
-scope = "leanprover"
-name = "Lean4Checker"
-rev = "b7398199245524275543dec6113229c9bb4902e5"
-
 [[require]]
 scope = "leanprover"
 name = "lean4export"