diff --git a/import-graph/ImportGraph/WorkspaceModel/Summary.lean b/import-graph/ImportGraph/WorkspaceModel/Summary.lean
index b16f9d24f..d201c3dd0 100644
--- a/import-graph/ImportGraph/WorkspaceModel/Summary.lean
+++ b/import-graph/ImportGraph/WorkspaceModel/Summary.lean
@@ -17,9 +17,7 @@ public import Lake.Util.Version
 ```
 These provide `Glob` and `ToolchainVer` in `WorkspaceSummary` field types. Cache validation also
 uses `Lake.Build.Trace` for hashing. None of these imports brings in Lake workspace loading or
-the build type-family axioms.
+the build type-family axioms; `ImportGraphTest.NoLakeAxioms` checks that.
 
 For Lake interaction with `WorkspaceSummary`, import `ImportGraph.WorkspaceModel.Summary.Lake`.
 -/
-
-assert_not_exists Lake.Workspace -- ensure we do not import deep lake internals