diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index ed2d060b19..7b3bc360a5 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -277,7 +277,8 @@ environment set_option_cmd(parser & p) {
         throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", p.pos());
     }
     p.updt_options();
-    return p.env();
+    environment env = p.env();
+    return update_fingerprint(env, p.get_options().hash());
 }
 
 static name parse_class(parser & p) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 2b02f8f756..d1cb9568d3 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -244,6 +244,7 @@ public:
     bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; }
 
     void updt_options();
+    options get_options() const { return m_ios.get_options(); }
     template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
 
     name mk_fresh_name() { return m_ngen.next(); }
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index 70464b95d3..6af4d6cdea 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -33,6 +33,7 @@ public:
     unsigned size() const;
     bool contains(name const & n) const;
     bool contains(char const * n) const;
+    unsigned hash() const { return m_value.hash(); }
 
     bool         get_bool(name const & n, bool default_value = false) const;
     int          get_int(name const & n, int default_value = 0) const;