diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 56aa9f1160..847f7c180f 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -43,6 +43,9 @@ add_test(NAME "lean_print_notation"
 add_test(NAME "auto_completion_issue_422"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./ac_bug.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "issue_597"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./issue_597.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/tests/lean/extra/597a.hlean b/tests/lean/extra/597a.hlean
new file mode 100644
index 0000000000..4bed446749
--- /dev/null
+++ b/tests/lean/extra/597a.hlean
@@ -0,0 +1,4 @@
+open equiv
+open equiv.ops
+constants (A B : Type₀) (f : A ≃ B)
+definition foo : A → B := f
diff --git a/tests/lean/extra/597b.hlean b/tests/lean/extra/597b.hlean
new file mode 100644
index 0000000000..c7bdb2583e
--- /dev/null
+++ b/tests/lean/extra/597b.hlean
@@ -0,0 +1,4 @@
+open equiv
+-- open equiv.ops
+constants (A B : Type₀) (f : A ≃ B)
+definition foo : A → B := f -- should fail
diff --git a/tests/lean/extra/issue_597.sh b/tests/lean/extra/issue_597.sh
new file mode 100755
index 0000000000..e0085b2e66
--- /dev/null
+++ b/tests/lean/extra/issue_597.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: bug_597.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export HLEAN_PATH=../../../hott
+"$LEAN" -c 597.clean 597a.hlean
+if "$LEAN" -c 597.clean 597b.hlean; then
+    echo "ERROR: using incorrect cached value..."
+    exit 1
+fi