diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 8a4667764d..de8e2a905e 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -127,7 +127,7 @@ structure SimpTheorem where
   deriving Inhabited
 
 mutual
-  partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
+  private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
     match type with
     | .forallE _ _ type _ =>
       if let .lam _ _ proof _ := proof then
@@ -144,23 +144,34 @@ mutual
         else if proof.getAppFn.isConst then
           -- The application of a `rfl` theorem is a `rfl` theorem
           -- A constant which is a `rfl` theorem is a `rfl` theorem
-          isRflTheorem proof.getAppFn.constName!
+          isRflTheoremCore proof.getAppFn.constName!
         else
           return false
       else
         return false
 
-  partial def isRflTheorem (declName : Name) : CoreM Bool := do
+  private partial def isRflTheoremCore (declName : Name) : CoreM Bool := do
     let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false
     let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false
     isRflProofCore info.type info.value
 end
 
+def isRflTheorem (declName : Name) : CoreM Bool :=
+  -- Make theorem body available if `declName` is from the current module; the body does not matter
+  -- for the ultimate application of a rfl theorem, only that the theorem type's LHS and RHS are
+  -- defeq.
+  withoutExporting do
+    isRflTheoremCore declName
+
 def isRflProof (proof : Expr) : MetaM Bool := do
-  if let .const declName .. := proof then
-    isRflTheorem declName
-  else
-    isRflProofCore (← inferType proof) proof
+  -- Make theorem body available if `declName` is from the current module; the body does not matter
+  -- for the ultimate application of a rfl theorem, only that the theorem type's LHS and RHS are
+  -- defeq.
+  withoutExporting do
+    if let .const declName .. := proof then
+      isRflTheoremCore declName
+    else
+      isRflProofCore (← inferType proof) proof
 
 instance : ToFormat SimpTheorem where
   format s :=
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index 3205214e2e..b64fc2dae6 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -1,7 +1,5 @@
 #include "util/options.h"
 
-// please update
-
 namespace lean {
 options get_default_options() {
     options opts;