diff --git a/.gitignore b/.gitignore
index bfb30ec..01f8cdb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/.lake
+.lake/
diff --git a/Main.lean b/Main.lean
index 3fe7c54..bd1c143 100644
--- a/Main.lean
+++ b/Main.lean
@@ -5,7 +5,7 @@ Authors: Henrik Böving
 -/
 import Lean
 import Comparator
-import Lean4Checker.Replay
+import Lean.Replay
 import Export.Parse
 
 namespace Comparator
@@ -198,7 +198,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/lake-manifest.json b/lake-manifest.json
index af32031..af47a1b 100644
--- a/lake-manifest.json
+++ b/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/lakefile.toml b/lakefile.toml
index 1865ae8..8b55152 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,11 +9,6 @@ name = "Comparator"
 name = "comparator"
 root = "Main"
 
-[[require]]
-scope = "leanprover"
-name = "Lean4Checker"
-rev = "b7398199245524275543dec6113229c9bb4902e5"
-
 [[require]]
 scope = "leanprover"
 name = "lean4export"